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  7049  oaass  7217  undom  7613  acndom2  8436  infxp  8596  isf32lem2  8735  ttukeylem3  8892  gchina  9075  r1limwun  9112  difreicc  11715  ssfzo12bi  11956  flflp1  11993  ccatcl  12668  wwlktovf1  12976  o1of2  13619  rlimsqzlem  13655  lcmgcdlem  14514  isprm5  14594  ramval  14903  ramvalOLD  14904  mreexexlem4d  15496  acsfn  15508  gsumpropd2lem  16459  gasubg  16899  psgndiflemB  19110  psgndiflemA  19111  mdetf  19562  cpmatacl  19682  cpmatinvcl  19683  mat2pmatf1  19695  mp2pm2mplem4  19775  chfacffsupp  19822  restcld  20130  cnpnei  20222  iscncl  20227  cncls  20232  cnntr  20233  1stcfb  20402  2ndcdisj  20413  txlly  20593  fbflim  20933  fclsbas  20978  nmoi  21675  nmoiOLD  21691  fgcfil  22183  equivcau  22212  cmetcusp  22263  itg2cnlem1  22661  iblss  22704  lgsqr  24216  axcontlem2  24937  usgra2wlkspth  25291  fargshiftfva  25309  constr3trllem2  25321  wlkiswwlk1  25360  wwlkext2clwwlk  25473  clwwisshclwwlem  25476  eupatrl  25638  frgra2v  25669  vdn1frgrav2  25695  vdgn1frgrav2  25696  frgrawopreg  25719  2spotiundisj  25732  usgreg2spot  25737  numclwlk1lem2f1  25764  numclwlk2lem2f1o  25775  blocnilem  26387  mdslmd3i  27927  foresf1o  28082  fgreu  28220  resf1o  28265  omndmul2  28426  psgnfzto1st  28570  fimaproj  28612  locfinreflem  28619  cmpcref  28629  pstmxmet  28652  lmdvg  28711  carsgclctunlem3  29104  oddpwdc  29139  sgnmul  29365  signstres  29416  cvmlift2lem12  29989  mrsubff  30102  elicc3  30922  nn0prpwlem  30927  neibastop2  30966  neibastop3  30967  ltflcei  31840  poimirlem4  31851  poimirlem13  31860  poimirlem14  31861  poimirlem26  31873  poimirlem27  31874  poimirlem28  31875  poimirlem29  31876  poimirlem31  31878  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  itg2addnclem  31900  itg2addnclem2  31901  itg2addnclem3  31902  itg2addnc  31903  itg2gt0cn  31904  ftc1cnnc  31923  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  nnubfi  31986  nninfnub  31987  linepsubN  33229  lhpmatb  33508  cdlemf2  34041  diaglbN  34535  diaintclN  34538  dibglbN  34646  dibintclN  34647  dihlsscpre  34714  dihglblem5aN  34772  dihglblem2aN  34773  dih1dimatlem  34809  diophren  35568  irrapxlem2  35580  irrapxlem4  35582  wepwsolem  35813  prmunb2  36572  cvgdvgrat  36575  fiiuncl  37322  icccncfext  37648  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  iblcncfioo  37738  wallispilem3  37812  fourierdlem12  37864  fourierdlem34  37887  fourierdlem50  37903  fourierdlem51  37904  fourierdlem65  37918  fourierdlem77  37930  hoicvr  38217  iccpartigtl  38550  iccpartgt  38554  opoeALTV  38625  opeoALTV  38626  nnsum4primeseven  38708  nnsum4primesevenALTV  38709  nbuhgr  39157  issubmgm2  39391  uzlidlring  39530  2zrngmmgm  39547  cznrng  39558  ply1mulgsumlem2  39782  snlindsntor  39867  elbigo2  39966  nn0sumshdiglemA  40033
  Copyright terms: Public domain W3C validator