Theorem ad3antlr 744

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 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	ad2antrr 739	1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simpllr  788  disjxiun  5099  fimaproj  8152  tfrlem1  8384  oaass  8570  acndom2  10134  infxp  10293  isf32lem2  10433  ttukeylem3  10590  gchina  10785  r1limwun  10822  difreicc  13616  ssfzo12bi  13897  flflp1  13948  hasheqf1oi  14496  ccatcl  14720  cshwidxmodr  14956  wwlktovf1  15111  sgnmul  15261  o1of2  15781  rlimsqzlem  15817  lcmgcdlem  16782  isprm5  16884  ramval  17187  mreexexlem4d  17822  acsfn  17834  chnso  18799  gsumpropd2lem  18869  issubmgm2  18893  gasubg  19517  omndmul2  20348  isdrng4  20993  unichnlidl  21517  qsidomlem1  21637  psgndiflemB  21907  psgndiflemA  21908  psrass1  22272  mhpmulcl  22471  mdetf  22911  matunitlindflem2  22996  cpmatacl  23035  cpmatinvcl  23036  mat2pmatf1  23048  mp2pm2mplem4  23128  chfacffsupp  23175  restcld  23491  cnpnei  23583  iscncl  23588  cncls  23593  cnntr  23594  1stcfb  23764  2ndcdisj  23776  txlly  23956  fbflim  24296  fclsbas  24341  nmoi  25048  mpomulcn  25189  fgcfil  25593  equivcau  25622  cmetcusp  25676  itg2cnlem1  26083  iblss  26126  lgsqr  27679  lgsqrmodndvds  27681  noetainflem4  28098  lesrec  28186  remulscllem2  28888  axcontlem2  29544  nbuhgr  29925  nbusgrvtxm1  29961  2pthon3v  30533  clwwisshclwwslem  30606  wwlksext2clwwlk  30649  2pthfrgr  30886  vdgn1frgrv2  30898  frgrwopreg  30925  numclwlk2lem2f1o  30981  blocnilem  31407  mdslmd3i  32935  foresf1o  33143  2ndresdju  33286  fgreu  33308  fdifsuppconst  33325  resf1o  33365  psgnfzto1st  33709  elrgspnsubrunlem1  33851  nsgqusf1olem3  34009  elrspunidl  34021  elrspunsn  34022  dflringlem3  34071  dflring4  34073  1arithidom  34112  dfufd2lem  34124  mplvrpmga  34220  lbsdiflsp0  34301  evls1fldgencl  34345  cos9thpiminplylem2  34458  ist0cld  34508  locfinreflem  34515  cmpcref  34525  zarclsun  34545  pstmxmet  34572  lmdvg  34628  carsgclctunlem3  34995  oddpwdc  35029  signstres  35247  tgoldbachgtd  35334  cvmlift2lem12  36148  satfdmlem  36202  satffunlem2lem1  36238  mrsubff  36346  elicc3  37180  nn0prpwlem  37185  neibastop2  37224  neibastop3  37225  mh-inf3f1  37404  bj-prmoore  38111  ltflcei  38607  poimirlem4  38618  poimirlem13  38627  poimirlem14  38628  poimirlem26  38640  poimirlem27  38641  poimirlem28  38642  poimirlem29  38643  poimirlem31  38645  heicant  38649  mblfinlem2  38652  mblfinlem3  38653  mblfinlem4  38654  ismblfin  38655  itg2addnclem  38665  itg2addnclem2  38666  itg2addnclem3  38667  itg2addnc  38668  itg2gt0cn  38669  ftc1cnnc  38686  ftc1anclem5  38691  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695  nnubfi  38760  nninfnub  38761  linepsubN  40885  lhpmatb  41164  cdlemf2  41695  diaglbN  42188  diaintclN  42191  dibglbN  42299  dibintclN  42300  dihlsscpre  42367  dihglblem5aN  42425  dihglblem2aN  42426  dih1dimatlem  42462  sticksstones12a  43283  fsuppind  43694  diophren  43896  irrapxlem2  43906  irrapxlem4  43908  wepwsolem  44125  omlimcl2  44320  tfsconcatfv  44419  ofoafg  44432  prmunb2  45371  cvgdvgrat  45373  fiiuncl  46158  infleinflem2  46458  supxrunb3  46486  supminfxr  46550  limsuppnflem  46796  limsupmnflem  46806  limsupre3lem  46818  dfxlim2v  46933  icccncfext  46973  ioodvbdlimc1lem1  47017  iblcncfioo  47064  wallispilem3  47153  fourierdlem12  47205  fourierdlem34  47227  fourierdlem50  47242  fourierdlem51  47243  fourierdlem65  47257  fourierdlem77  47269  meaiuninc3v  47570  hspdifhsp  47702  smflimlem4  47860  iccpartigtl  48581  iccpartgt  48585  fargshiftfva  48601  sfprmdvdsmersenne  48764  opoeALTV  48857  opeoALTV  48858  nnsum4primeseven  48974  nnsum4primesevenALTV  48975  uhgrimedgi  49064  isuspgrimlem  49069  gricushgr  49091  isubgr3stgrlem7  49146  uspgrlimlem4  49165  gpgedgvtx1  49236  pgn4cyclex  49300  uzlidlring  49408  2zrngmmgm  49425  cznrng  49434  ply1mulgsumlem2  49575  snlindsntor  49659  elbigo2  49740  nn0sumshdiglemA  49807  precofvalALT  50552