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

Theorem ad3antlr 735
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 731 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 466 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad4antlr  737  tfrlem1  7102  oaass  7270  undom  7666  acndom2  8483  infxp  8643  isf32lem2  8782  ttukeylem3  8939  gchina  9123  r1limwun  9160  difreicc  11762  ssfzo12bi  12003  flflp1  12040  ccatcl  12707  wwlktovf1  13011  o1of2  13654  rlimsqzlem  13690  lcmgcdlem  14542  isprm5  14622  ramval  14923  ramvalOLD  14924  mreexexlem4d  15504  acsfn  15516  gsumpropd2lem  16467  gasubg  16907  psgndiflemB  19099  psgndiflemA  19100  mdetf  19551  cpmatacl  19671  cpmatinvcl  19672  mat2pmatf1  19684  mp2pm2mplem4  19764  chfacffsupp  19811  restcld  20119  cnpnei  20211  iscncl  20216  cncls  20221  cnntr  20222  1stcfb  20391  2ndcdisj  20402  txlly  20582  fbflim  20922  fclsbas  20967  nmoi  21660  fgcfil  22134  equivcau  22163  cmetcusp  22214  itg2cnlem1  22596  iblss  22639  lgsqr  24137  axcontlem2  24841  usgra2wlkspth  25194  fargshiftfva  25212  constr3trllem2  25224  wlkiswwlk1  25263  wwlkext2clwwlk  25376  clwwisshclwwlem  25379  eupatrl  25541  frgra2v  25572  vdn1frgrav2  25598  vdgn1frgrav2  25599  frgrawopreg  25622  2spotiundisj  25635  usgreg2spot  25640  numclwlk1lem2f1  25667  numclwlk2lem2f1o  25678  blocnilem  26290  mdslmd3i  27820  foresf1o  27975  fgreu  28114  resf1o  28158  omndmul2  28313  psgnfzto1st  28457  fimaproj  28499  locfinreflem  28506  cmpcref  28516  pstmxmet  28539  lmdvg  28598  carsgclctunlem3  28981  oddpwdc  29013  sgnmul  29201  signstres  29252  cvmlift2lem12  29825  mrsubff  29938  elicc3  30758  nn0prpwlem  30763  neibastop2  30802  neibastop3  30803  ltflcei  31636  poimirlem4  31647  poimirlem13  31656  poimirlem14  31657  poimirlem26  31669  poimirlem27  31670  poimirlem28  31671  poimirlem29  31672  poimirlem31  31674  heicant  31678  mblfinlem2  31681  mblfinlem3  31682  mblfinlem4  31683  ismblfin  31684  itg2addnclem  31696  itg2addnclem2  31697  itg2addnclem3  31698  itg2addnc  31699  itg2gt0cn  31700  ftc1cnnc  31719  ftc1anclem5  31724  ftc1anclem6  31725  ftc1anclem7  31726  ftc1anclem8  31727  ftc1anc  31728  nnubfi  31782  nninfnub  31783  linepsubN  33025  lhpmatb  33304  cdlemf2  33837  diaglbN  34331  diaintclN  34334  dibglbN  34442  dibintclN  34443  dihlsscpre  34510  dihglblem5aN  34568  dihglblem2aN  34569  dih1dimatlem  34605  diophren  35364  irrapxlem2  35376  irrapxlem4  35378  wepwsolem  35605  prmunb2  36295  cvgdvgrat  36298  fiiuncl  37047  icccncfext  37336  ioodvbdlimc1lem1  37374  iblcncfioo  37423  wallispilem3  37497  fourierdlem12  37549  fourierdlem34  37571  fourierdlem50  37587  fourierdlem51  37588  fourierdlem65  37602  fourierdlem77  37614  iccpartigtl  38126  iccpartgt  38130  opoeALTV  38201  opeoALTV  38202  nnsum4primeseven  38284  nnsum4primesevenALTV  38285  issubmgm2  38547  uzlidlring  38686  2zrngmmgm  38703  cznrng  38714  ply1mulgsumlem2  38938  snlindsntor  39023  elbigo2  39123  nn0sumshdiglemA  39190
  Copyright terms: Public domain W3C validator