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

Theorem ad3antlr 730
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 483 . 2 ((𝜒𝜑) → 𝜓)
32ad2antrr 725 1 ((((𝜒𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  simpllr  775  disjxiun  5103  fimaproj  8068  tfrlem1  8323  oaass  8509  undomOLD  9005  acndom2  9991  infxp  10152  isf32lem2  10291  ttukeylem3  10448  gchina  10636  r1limwun  10673  difreicc  13402  ssfzo12bi  13668  flflp1  13713  hasheqf1oi  14252  ccatcl  14463  cshwidxmodr  14693  wwlktovf1  14847  o1of2  15496  rlimsqzlem  15534  lcmgcdlem  16483  isprm5  16584  ramval  16881  mreexexlem4d  17528  acsfn  17540  gsumpropd2lem  18535  gasubg  19083  psgndiflemB  21007  psgndiflemA  21008  mdetf  21947  cpmatacl  22068  cpmatinvcl  22069  mat2pmatf1  22081  mp2pm2mplem4  22161  chfacffsupp  22208  restcld  22526  cnpnei  22618  iscncl  22623  cncls  22628  cnntr  22629  1stcfb  22799  2ndcdisj  22810  txlly  22990  fbflim  23330  fclsbas  23375  nmoi  24095  fgcfil  24638  equivcau  24667  cmetcusp  24721  itg2cnlem1  25129  iblss  25172  lgsqr  26702  lgsqrmodndvds  26704  noetainflem4  27091  slerec  27161  axcontlem2  27917  nbuhgr  28294  nbusgrvtxm1  28330  2pthon3v  28891  clwwisshclwwslem  28961  wwlksext2clwwlk  29004  2pthfrgr  29231  vdgn1frgrv2  29243  frgrwopreg  29270  numclwlk2lem2f1o  29326  blocnilem  29749  mdslmd3i  31277  foresf1o  31434  2ndresdju  31568  fgreu  31591  fdifsuppconst  31607  resf1o  31650  omndmul2  31923  psgnfzto1st  31957  nsgqusf1olem3  32196  elrspunidl  32206  qsidomlem1  32228  lbsdiflsp0  32324  ist0cld  32417  locfinreflem  32424  cmpcref  32434  zarclsun  32454  pstmxmet  32481  lmdvg  32537  carsgclctunlem3  32923  oddpwdc  32957  sgnmul  33145  signstres  33190  tgoldbachgtd  33278  cvmlift2lem12  33911  satfdmlem  33965  satffunlem2lem1  34001  mrsubff  34109  elicc3  34792  nn0prpwlem  34797  neibastop2  34836  neibastop3  34837  bj-prmoore  35589  ltflcei  36069  matunitlindflem2  36078  poimirlem4  36085  poimirlem13  36094  poimirlem14  36095  poimirlem26  36107  poimirlem27  36108  poimirlem28  36109  poimirlem29  36110  poimirlem31  36112  heicant  36116  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  itg2addnclem  36132  itg2addnclem2  36133  itg2addnclem3  36134  itg2addnc  36135  itg2gt0cn  36136  ftc1cnnc  36153  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  nnubfi  36212  nninfnub  36213  linepsubN  38218  lhpmatb  38497  cdlemf2  39028  diaglbN  39521  diaintclN  39524  dibglbN  39632  dibintclN  39633  dihlsscpre  39700  dihglblem5aN  39758  dihglblem2aN  39759  dih1dimatlem  39795  sticksstones12a  40568  fsuppind  40768  diophren  41139  irrapxlem2  41149  irrapxlem4  41151  wepwsolem  41372  omlimcl2  41579  ofoafg  41671  prmunb2  42598  cvgdvgrat  42600  fiiuncl  43280  infleinflem2  43612  supxrunb3  43641  supminfxr  43706  limsuppnflem  43958  limsupmnflem  43968  limsupre3lem  43980  dfxlim2v  44095  icccncfext  44135  ioodvbdlimc1lem1  44179  iblcncfioo  44226  wallispilem3  44315  fourierdlem12  44367  fourierdlem34  44389  fourierdlem50  44404  fourierdlem51  44405  fourierdlem65  44419  fourierdlem77  44431  meaiuninc3v  44732  hoicvr  44796  hspdifhsp  44864  smflimlem4  45022  iccpartigtl  45622  iccpartgt  45626  fargshiftfva  45642  sfprmdvdsmersenne  45802  opoeALTV  45882  opeoALTV  45883  nnsum4primeseven  45999  nnsum4primesevenALTV  46000  isomushgr  46025  isomuspgr  46033  issubmgm2  46091  uzlidlring  46234  2zrngmmgm  46251  cznrng  46260  ply1mulgsumlem2  46475  snlindsntor  46559  elbigo2  46645  nn0sumshdiglemA  46712
  Copyright terms: Public domain W3C validator