Theorem ad3antlr 729

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

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 484	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 724	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simpllr  774  disjxiun  5055  fimaproj  7823  tfrlem1  8006  oaass  8181  undom  8599  acndom2  9474  infxp  9631  isf32lem2  9770  ttukeylem3  9927  gchina  10115  r1limwun  10152  difreicc  12864  ssfzo12bi  13126  flflp1  13171  hasheqf1oi  13706  ccatcl  13920  cshwidxmodr  14160  wwlktovf1  14315  o1of2  14963  rlimsqzlem  14999  lcmgcdlem  15944  isprm5  16045  ramval  16338  mreexexlem4d  16912  acsfn  16924  gsumpropd2lem  17883  gasubg  18426  psgndiflemB  20738  psgndiflemA  20739  mdetf  21198  cpmatacl  21318  cpmatinvcl  21319  mat2pmatf1  21331  mp2pm2mplem4  21411  chfacffsupp  21458  restcld  21774  cnpnei  21866  iscncl  21871  cncls  21876  cnntr  21877  1stcfb  22047  2ndcdisj  22058  txlly  22238  fbflim  22578  fclsbas  22623  nmoi  23331  fgcfil  23868  equivcau  23897  cmetcusp  23951  itg2cnlem1  24356  iblss  24399  lgsqr  25921  lgsqrmodndvds  25923  axcontlem2  26745  nbuhgr  27119  nbusgrvtxm1  27155  2pthon3v  27716  clwwisshclwwslem  27786  wwlksext2clwwlk  27830  2pthfrgr  28057  vdgn1frgrv2  28069  frgrwopreg  28096  numclwlk2lem2f1o  28152  blocnilem  28575  mdslmd3i  30103  foresf1o  30259  fgreu  30411  resf1o  30460  omndmul2  30708  psgnfzto1st  30742  qsidomlem1  30960  lbsdiflsp0  31017  locfinreflem  31099  cmpcref  31109  pstmxmet  31132  lmdvg  31191  carsgclctunlem3  31573  oddpwdc  31607  sgnmul  31795  signstres  31840  tgoldbachgtd  31928  cvmlift2lem12  32556  satfdmlem  32610  satffunlem2lem1  32646  mrsubff  32754  slerec  33272  elicc3  33660  nn0prpwlem  33665  neibastop2  33704  neibastop3  33705  bj-prmoore  34401  ltflcei  34874  matunitlindflem2  34883  poimirlem4  34890  poimirlem13  34899  poimirlem14  34900  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  poimirlem29  34915  poimirlem31  34917  heicant  34921  mblfinlem2  34924  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  itg2addnclem  34937  itg2addnclem2  34938  itg2addnclem3  34939  itg2addnc  34940  itg2gt0cn  34941  ftc1cnnc  34960  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  nnubfi  35019  nninfnub  35020  linepsubN  36882  lhpmatb  37161  cdlemf2  37692  diaglbN  38185  diaintclN  38188  dibglbN  38296  dibintclN  38297  dihlsscpre  38364  dihglblem5aN  38422  dihglblem2aN  38423  dih1dimatlem  38459  diophren  39403  irrapxlem2  39413  irrapxlem4  39415  wepwsolem  39635  prmunb2  40636  cvgdvgrat  40638  fiiuncl  41320  infleinflem2  41632  supxrunb3  41665  supminfxr  41733  limsuppnflem  41984  limsupmnflem  41994  limsupre3lem  42006  dfxlim2v  42121  icccncfext  42163  ioodvbdlimc1lem1  42209  iblcncfioo  42256  wallispilem3  42346  fourierdlem12  42398  fourierdlem34  42420  fourierdlem50  42435  fourierdlem51  42436  fourierdlem65  42450  fourierdlem77  42462  meaiuninc3v  42760  hoicvr  42824  hspdifhsp  42892  smflimlem4  43044  iccpartigtl  43577  iccpartgt  43581  fargshiftfva  43597  sfprmdvdsmersenne  43762  opoeALTV  43842  opeoALTV  43843  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  isomushgr  43985  isomuspgr  43993  issubmgm2  44051  uzlidlring  44194  2zrngmmgm  44211  cznrng  44220  ply1mulgsumlem2  44435  snlindsntor  44520  elbigo2  44606  nn0sumshdiglemA  44673