MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad3antlr Structured version   Unicode version

Theorem ad3antlr 713
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad3antlr  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21ad2antlr 709 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 453 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad4antlr  715  oaass  6805  undom  7197  acndom2  7936  infxp  8096  isf32lem2  8235  ttukeylem3  8392  gchina  8575  r1limwun  8612  difreicc  11029  o1of2  12407  rlimsqzlem  12443  isprm5  13113  ramval  13377  mreexexlem4d  13873  acsfn  13885  gasubg  15080  restcld  17237  cnpnei  17329  iscncl  17334  cncls  17339  cnntr  17340  1stcfb  17509  2ndcdisj  17520  txlly  17669  fbflim  18009  fclsbas  18054  nmoi  18763  fgcfil  19225  equivcau  19254  cmetcuspOLD  19308  cmetcusp  19309  itg2cnlem1  19654  iblss  19697  lgsqr  21131  fargshiftfva  21627  constr3trllem2  21639  eupatrl  21691  blocnilem  22306  mdslmd3i  23836  gsumpropd2lem  24221  pstmxmet  24293  lmdvg  24339  cvmlift2lem12  25002  axcontlem2  25905  ltflcei  26240  lxflflp1  26242  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  ismblfin  26248  itg2addnclem  26257  itg2addnclem2  26258  itg2addnclem3  26259  itg2addnc  26260  itg2gt0cn  26261  ftc1cnnc  26280  ftc1anclem5  26285  ftc1anclem6  26286  ftc1anclem7  26287  ftc1anclem8  26288  ftc1anc  26289  elicc3  26321  nn0prpwlem  26326  neibastop2  26391  neibastop3  26392  nnubfi  26455  nninfnub  26456  diophren  26875  irrapxlem2  26887  irrapxlem4  26889  wepwsolem  27117  wallispilem3  27793  cshwidx  28243  usgra2wlkspth  28309  vdn1frgrav2  28417  vdgn1frgrav2  28418  frgrawopreg  28439  2spotiundisj  28452  usgreg2spot  28457  linepsubN  30550  lhpmatb  30829  cdlemf2  31360  diaglbN  31854  diaintclN  31857  dibglbN  31965  dibintclN  31966  dihlsscpre  32033  dihglblem5aN  32091  dihglblem2aN  32092  dih1dimatlem  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator