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

Theorem ad3antlr 742
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 738 . 2  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
32adantr 471 1  |-  ( ( ( ( ch  /\  ph )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad4antlr  744  tfrlem1  7119  oaass  7287  undom  7685  acndom2  8510  infxp  8670  isf32lem2  8809  ttukeylem3  8966  gchina  9149  r1limwun  9186  difreicc  11792  ssfzo12bi  12036  flflp1  12074  ccatcl  12755  wwlktovf1  13080  o1of2  13724  rlimsqzlem  13760  lcmgcdlem  14619  isprm5  14699  ramval  15008  ramvalOLD  15009  mreexexlem4d  15601  acsfn  15613  gsumpropd2lem  16564  gasubg  17004  psgndiflemB  19216  psgndiflemA  19217  mdetf  19668  cpmatacl  19788  cpmatinvcl  19789  mat2pmatf1  19801  mp2pm2mplem4  19881  chfacffsupp  19928  restcld  20236  cnpnei  20328  iscncl  20333  cncls  20338  cnntr  20339  1stcfb  20508  2ndcdisj  20519  txlly  20699  fbflim  21039  fclsbas  21084  nmoi  21781  nmoiOLD  21797  fgcfil  22289  equivcau  22318  cmetcusp  22369  itg2cnlem1  22767  iblss  22810  lgsqr  24322  axcontlem2  25043  usgra2wlkspth  25397  fargshiftfva  25415  constr3trllem2  25427  wlkiswwlk1  25466  wwlkext2clwwlk  25579  clwwisshclwwlem  25582  eupatrl  25744  frgra2v  25775  vdn1frgrav2  25801  vdgn1frgrav2  25802  frgrawopreg  25825  2spotiundisj  25838  usgreg2spot  25843  numclwlk1lem2f1  25870  numclwlk2lem2f1o  25881  blocnilem  26493  mdslmd3i  28033  foresf1o  28187  fgreu  28322  resf1o  28363  omndmul2  28523  psgnfzto1st  28666  fimaproj  28708  locfinreflem  28715  cmpcref  28725  pstmxmet  28748  lmdvg  28807  carsgclctunlem3  29200  oddpwdc  29235  sgnmul  29461  signstres  29512  cvmlift2lem12  30085  mrsubff  30198  elicc3  31021  nn0prpwlem  31026  neibastop2  31065  neibastop3  31066  ltflcei  31977  poimirlem4  31988  poimirlem13  31997  poimirlem14  31998  poimirlem26  32010  poimirlem27  32011  poimirlem28  32012  poimirlem29  32013  poimirlem31  32015  heicant  32019  mblfinlem2  32022  mblfinlem3  32023  mblfinlem4  32024  ismblfin  32025  itg2addnclem  32037  itg2addnclem2  32038  itg2addnclem3  32039  itg2addnc  32040  itg2gt0cn  32041  ftc1cnnc  32060  ftc1anclem5  32065  ftc1anclem6  32066  ftc1anclem7  32067  ftc1anclem8  32068  ftc1anc  32069  nnubfi  32123  nninfnub  32124  linepsubN  33361  lhpmatb  33640  cdlemf2  34173  diaglbN  34667  diaintclN  34670  dibglbN  34778  dibintclN  34779  dihlsscpre  34846  dihglblem5aN  34904  dihglblem2aN  34905  dih1dimatlem  34941  diophren  35700  irrapxlem2  35711  irrapxlem4  35713  wepwsolem  35944  prmunb2  36702  cvgdvgrat  36705  fiiuncl  37443  icccncfext  37802  ioodvbdlimc1lem1  37840  ioodvbdlimc1lem1OLD  37842  iblcncfioo  37892  wallispilem3  37966  fourierdlem12  38018  fourierdlem34  38041  fourierdlem50  38057  fourierdlem51  38058  fourierdlem65  38072  fourierdlem77  38084  hoicvr  38407  hspdifhsp  38475  iccpartigtl  38774  iccpartgt  38778  opoeALTV  38849  opeoALTV  38850  nnsum4primeseven  38932  nnsum4primesevenALTV  38933  nbuhgr  39460  nbusgrvtxm1  39502  2pthon3v-av  39891  issubmgm2  40062  uzlidlring  40201  2zrngmmgm  40218  cznrng  40229  ply1mulgsumlem2  40451  snlindsntor  40536  elbigo2  40635  nn0sumshdiglemA  40702
  Copyright terms: Public domain W3C validator