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

Theorem ad3antlr 727
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antlr ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antlr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantl 482 . 2 ((𝜒𝜑) → 𝜓)
32ad2antrr 722 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  simpllr  772  disjxiun  5059  fimaproj  7823  tfrlem1  8006  oaass  8180  undom  8597  acndom2  9472  infxp  9629  isf32lem2  9768  ttukeylem3  9925  gchina  10113  r1limwun  10150  difreicc  12863  ssfzo12bi  13125  flflp1  13170  hasheqf1oi  13705  ccatcl  13919  cshwidxmodr  14159  wwlktovf1  14314  o1of2  14962  rlimsqzlem  14998  lcmgcdlem  15942  isprm5  16043  ramval  16336  mreexexlem4d  16910  acsfn  16922  gsumpropd2lem  17880  gasubg  18364  psgndiflemB  20662  psgndiflemA  20663  mdetf  21122  cpmatacl  21242  cpmatinvcl  21243  mat2pmatf1  21255  mp2pm2mplem4  21335  chfacffsupp  21382  restcld  21698  cnpnei  21790  iscncl  21795  cncls  21800  cnntr  21801  1stcfb  21971  2ndcdisj  21982  txlly  22162  fbflim  22502  fclsbas  22547  nmoi  23254  fgcfil  23791  equivcau  23820  cmetcusp  23874  itg2cnlem1  24279  iblss  24322  lgsqr  25843  lgsqrmodndvds  25845  axcontlem2  26667  nbuhgr  27041  nbusgrvtxm1  27077  2pthon3v  27638  clwwisshclwwslem  27708  wwlksext2clwwlk  27752  2pthfrgr  27979  vdgn1frgrv2  27991  frgrwopreg  28018  numclwlk2lem2f1o  28074  blocnilem  28497  mdslmd3i  30025  foresf1o  30181  fgreu  30334  resf1o  30381  omndmul2  30629  psgnfzto1st  30663  qsidomlem1  30871  lbsdiflsp0  30910  locfinreflem  30992  cmpcref  31002  pstmxmet  31025  lmdvg  31084  carsgclctunlem3  31466  oddpwdc  31500  sgnmul  31688  signstres  31733  tgoldbachgtd  31821  cvmlift2lem12  32447  satfdmlem  32501  satffunlem2lem1  32537  mrsubff  32645  slerec  33163  elicc3  33551  nn0prpwlem  33556  neibastop2  33595  neibastop3  33596  ltflcei  34749  matunitlindflem2  34758  poimirlem4  34765  poimirlem13  34774  poimirlem14  34775  poimirlem26  34787  poimirlem27  34788  poimirlem28  34789  poimirlem29  34790  poimirlem31  34792  heicant  34796  mblfinlem2  34799  mblfinlem3  34800  mblfinlem4  34801  ismblfin  34802  itg2addnclem  34812  itg2addnclem2  34813  itg2addnclem3  34814  itg2addnc  34815  itg2gt0cn  34816  ftc1cnnc  34835  ftc1anclem5  34840  ftc1anclem6  34841  ftc1anclem7  34842  ftc1anclem8  34843  ftc1anc  34844  nnubfi  34895  nninfnub  34896  linepsubN  36757  lhpmatb  37036  cdlemf2  37567  diaglbN  38060  diaintclN  38063  dibglbN  38171  dibintclN  38172  dihlsscpre  38239  dihglblem5aN  38297  dihglblem2aN  38298  dih1dimatlem  38334  diophren  39277  irrapxlem2  39287  irrapxlem4  39289  wepwsolem  39509  prmunb2  40510  cvgdvgrat  40512  fiiuncl  41194  infleinflem2  41506  supxrunb3  41539  supminfxr  41607  limsuppnflem  41858  limsupmnflem  41868  limsupre3lem  41880  dfxlim2v  41995  icccncfext  42037  ioodvbdlimc1lem1  42083  iblcncfioo  42130  wallispilem3  42220  fourierdlem12  42272  fourierdlem34  42294  fourierdlem50  42309  fourierdlem51  42310  fourierdlem65  42324  fourierdlem77  42336  meaiuninc3v  42634  hoicvr  42698  hspdifhsp  42766  smflimlem4  42918  iccpartigtl  43417  iccpartgt  43421  fargshiftfva  43437  sfprmdvdsmersenne  43602  opoeALTV  43682  opeoALTV  43683  nnsum4primeseven  43799  nnsum4primesevenALTV  43800  isomushgr  43825  isomuspgr  43833  issubmgm2  43891  uzlidlring  44034  2zrngmmgm  44051  cznrng  44060  ply1mulgsumlem2  44275  snlindsntor  44360  elbigo2  44446  nn0sumshdiglemA  44513
  Copyright terms: Public domain W3C validator