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

Theorem ad3antlr 767
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 481 . 2 ((𝜒𝜑) → 𝜓)
32ad2antrr 762 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad4antlrOLD  772  simpllr  815  disjxiun  4681  tfrlem1  7517  oaass  7686  undom  8089  acndom2  8915  infxp  9075  isf32lem2  9214  ttukeylem3  9371  gchina  9559  r1limwun  9596  difreicc  12342  ssfzo12bi  12603  flflp1  12648  hasheqf1oi  13180  ccatcl  13392  cshwidxmodr  13596  wwlktovf1  13746  o1of2  14387  rlimsqzlem  14423  lcmgcdlem  15366  isprm5  15466  ramval  15759  mreexexlem4d  16354  acsfn  16367  gsumpropd2lem  17320  gasubg  17781  psgndiflemB  19994  psgndiflemA  19995  mdetf  20449  cpmatacl  20569  cpmatinvcl  20570  mat2pmatf1  20582  mp2pm2mplem4  20662  chfacffsupp  20709  restcld  21024  cnpnei  21116  iscncl  21121  cncls  21126  cnntr  21127  1stcfb  21296  2ndcdisj  21307  txlly  21487  fbflim  21827  fclsbas  21872  nmoi  22579  fgcfil  23115  equivcau  23144  cmetcusp  23196  itg2cnlem1  23573  iblss  23616  lgsqr  25121  lgsqrmodndvds  25123  axcontlem2  25890  nbuhgr  26284  nbusgrvtxm1  26325  2pthon3v  26908  clwwisshclwwslem  26971  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  2pthfrgr  27264  vdgn1frgrv2  27276  frgrwopreg  27303  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  blocnilem  27787  mdslmd3i  29319  foresf1o  29469  fgreu  29599  resf1o  29633  omndmul2  29840  psgnfzto1st  29983  fimaproj  30028  locfinreflem  30035  cmpcref  30045  pstmxmet  30068  lmdvg  30127  carsgclctunlem3  30510  oddpwdc  30544  sgnmul  30732  signstres  30780  tgoldbachgtd  30868  cvmlift2lem12  31422  mrsubff  31535  slerec  32048  elicc3  32436  nn0prpwlem  32442  neibastop2  32481  neibastop3  32482  ltflcei  33527  matunitlindflem2  33536  poimirlem4  33543  poimirlem13  33552  poimirlem14  33553  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  ftc1cnnc  33614  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  nnubfi  33676  nninfnub  33677  linepsubN  35356  lhpmatb  35635  cdlemf2  36167  diaglbN  36661  diaintclN  36664  dibglbN  36772  dibintclN  36773  dihlsscpre  36840  dihglblem5aN  36898  dihglblem2aN  36899  dih1dimatlem  36935  diophren  37694  irrapxlem2  37704  irrapxlem4  37706  wepwsolem  37929  prmunb2  38827  cvgdvgrat  38829  fiiuncl  39548  infleinflem2  39900  supxrunb3  39936  supminfxr  40007  limsuppnflem  40260  limsupmnflem  40270  limsupre3lem  40282  dfxlim2v  40391  icccncfext  40418  ioodvbdlimc1lem1  40464  iblcncfioo  40512  wallispilem3  40602  fourierdlem12  40654  fourierdlem34  40676  fourierdlem50  40691  fourierdlem51  40692  fourierdlem65  40706  fourierdlem77  40718  meaiuninc3v  41019  hoicvr  41083  hspdifhsp  41151  smflimlem4  41303  iccpartigtl  41684  iccpartgt  41688  fargshiftfva  41704  sfprmdvdsmersenne  41845  opoeALTV  41919  opeoALTV  41920  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  issubmgm2  42115  uzlidlring  42254  2zrngmmgm  42271  cznrng  42280  ply1mulgsumlem2  42500  snlindsntor  42585  elbigo2  42671  nn0sumshdiglemA  42738
  Copyright terms: Public domain W3C validator