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

Theorem ad3antlr 730
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 726 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 465 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ad4antlr  732  oaass  7012  undom  7411  acndom2  8236  infxp  8396  isf32lem2  8535  ttukeylem3  8692  gchina  8878  r1limwun  8915  difreicc  11429  ssfzo12bi  11634  o1of2  13102  rlimsqzlem  13138  isprm5  13810  ramval  14081  mreexexlem4d  14597  acsfn  14609  gsumpropd2lem  15517  gasubg  15832  psgndiflemB  18042  psgndiflemA  18043  mdetf  18418  restcld  18788  cnpnei  18880  iscncl  18885  cncls  18890  cnntr  18891  1stcfb  19061  2ndcdisj  19072  txlly  19221  fbflim  19561  fclsbas  19606  nmoi  20319  fgcfil  20794  equivcau  20823  cmetcuspOLD  20877  cmetcusp  20878  itg2cnlem1  21251  iblss  21294  lgsqr  22697  axcontlem2  23223  fargshiftfva  23537  constr3trllem2  23549  eupatrl  23601  blocnilem  24216  mdslmd3i  25748  fgreu  26002  resf1o  26042  omndmul2  26187  pstmxmet  26336  lmdvg  26395  oddpwdc  26749  sgnmul  26937  signstres  26988  cvmlift2lem12  27215  ltflcei  28431  lxflflp1  28433  heicant  28438  mblfinlem2  28441  mblfinlem3  28442  mblfinlem4  28443  ismblfin  28444  itg2addnclem  28455  itg2addnclem2  28456  itg2addnclem3  28457  itg2addnc  28458  itg2gt0cn  28459  ftc1cnnc  28478  ftc1anclem5  28483  ftc1anclem6  28484  ftc1anclem7  28485  ftc1anclem8  28486  ftc1anc  28487  elicc3  28524  nn0prpwlem  28529  neibastop2  28594  neibastop3  28595  nnubfi  28658  nninfnub  28659  diophren  29164  irrapxlem2  29176  irrapxlem4  29178  wepwsolem  29406  wallispilem3  29874  wwlktovf1  30264  usgra2wlkspth  30310  wlkiswwlk1  30336  wwlkext2clwwlk  30477  clwwisshclwwlem  30482  frgra2v  30603  vdn1frgrav2  30630  vdgn1frgrav2  30631  frgrawopreg  30654  2spotiundisj  30667  usgreg2spot  30672  numclwlk1lem2f1  30699  numclwlk2lem2f1o  30710  ply1mulgsumlem2  30857  scmatsubcl  30896  mp2pm2mplem4  30931  snlindsntor  31017  linepsubN  33408  lhpmatb  33687  cdlemf2  34218  diaglbN  34712  diaintclN  34715  dibglbN  34823  dibintclN  34824  dihlsscpre  34891  dihglblem5aN  34949  dihglblem2aN  34950  dih1dimatlem  34986
  Copyright terms: Public domain W3C validator