Theorem ad3antlr 737

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

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  781  disjxiun  5076  fimaproj  8082  tfrlem1  8312  oaass  8493  acndom2  9974  infxp  10134  isf32lem2  10274  ttukeylem3  10431  gchina  10620  r1limwun  10657  difreicc  13435  ssfzo12bi  13714  flflp1  13764  hasheqf1oi  14311  ccatcl  14534  cshwidxmodr  14764  wwlktovf1  14917  o1of2  15573  rlimsqzlem  15609  lcmgcdlem  16573  isprm5  16675  ramval  16977  mreexexlem4d  17611  acsfn  17623  chnso  18588  gsumpropd2lem  18645  issubmgm2  18669  gasubg  19275  omndmul2  20106  psgndiflemB  21582  psgndiflemA  21583  psrass1  21945  mhpmulcl  22144  mdetf  22585  cpmatacl  22706  cpmatinvcl  22707  mat2pmatf1  22719  mp2pm2mplem4  22799  chfacffsupp  22846  restcld  23162  cnpnei  23254  iscncl  23259  cncls  23264  cnntr  23265  1stcfb  23435  2ndcdisj  23446  txlly  23626  fbflim  23966  fclsbas  24011  nmoi  24718  mpomulcn  24859  fgcfil  25263  equivcau  25292  cmetcusp  25346  itg2cnlem1  25753  iblss  25797  lgsqr  27339  lgsqrmodndvds  27341  noetainflem4  27729  lesrec  27816  remulscllem2  28518  axcontlem2  29059  nbuhgr  29437  nbusgrvtxm1  29473  2pthon3v  30036  clwwisshclwwslem  30109  wwlksext2clwwlk  30152  2pthfrgr  30379  vdgn1frgrv2  30391  frgrwopreg  30418  numclwlk2lem2f1o  30474  blocnilem  30900  mdslmd3i  32428  foresf1o  32599  2ndresdju  32748  fgreu  32770  fdifsuppconst  32788  resf1o  32829  sgnmul  32934  psgnfzto1st  33193  elrgspnsubrunlem1  33335  isdrng4  33386  nsgqusf1olem3  33505  elrspunidl  33518  elrspunsn  33519  qsidomlem1  33542  1arithidom  33627  dfufd2lem  33639  mplvrpmga  33736  lbsdiflsp0  33817  evls1fldgencl  33861  cos9thpiminplylem2  33974  ist0cld  34024  locfinreflem  34031  cmpcref  34041  zarclsun  34061  pstmxmet  34088  lmdvg  34144  carsgclctunlem3  34511  oddpwdc  34545  signstres  34766  tgoldbachgtd  34853  cvmlift2lem12  35543  satfdmlem  35597  satffunlem2lem1  35633  mrsubff  35741  elicc3  36546  nn0prpwlem  36551  neibastop2  36590  neibastop3  36591  bj-prmoore  37474  ltflcei  37976  matunitlindflem2  37985  poimirlem4  37992  poimirlem13  38001  poimirlem14  38002  poimirlem26  38014  poimirlem27  38015  poimirlem28  38016  poimirlem29  38017  poimirlem31  38019  heicant  38023  mblfinlem2  38026  mblfinlem3  38027  mblfinlem4  38028  ismblfin  38029  itg2addnclem  38039  itg2addnclem2  38040  itg2addnclem3  38041  itg2addnc  38042  itg2gt0cn  38043  ftc1cnnc  38060  ftc1anclem5  38065  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  nnubfi  38118  nninfnub  38119  linepsubN  40245  lhpmatb  40524  cdlemf2  41055  diaglbN  41548  diaintclN  41551  dibglbN  41659  dibintclN  41660  dihlsscpre  41727  dihglblem5aN  41785  dihglblem2aN  41786  dih1dimatlem  41822  sticksstones12a  42643  fsuppind  43041  diophren  43259  irrapxlem2  43269  irrapxlem4  43271  wepwsolem  43488  omlimcl2  43688  tfsconcatfv  43787  ofoafg  43800  prmunb2  44756  cvgdvgrat  44758  fiiuncl  45514  infleinflem2  45816  supxrunb3  45844  supminfxr  45908  limsuppnflem  46154  limsupmnflem  46164  limsupre3lem  46176  dfxlim2v  46291  icccncfext  46331  ioodvbdlimc1lem1  46375  iblcncfioo  46422  wallispilem3  46511  fourierdlem12  46563  fourierdlem34  46585  fourierdlem50  46600  fourierdlem51  46601  fourierdlem65  46615  fourierdlem77  46627  meaiuninc3v  46928  hspdifhsp  47060  smflimlem4  47218  iccpartigtl  47899  iccpartgt  47903  fargshiftfva  47919  sfprmdvdsmersenne  48082  opoeALTV  48175  opeoALTV  48176  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  uhgrimedgi  48382  isuspgrimlem  48387  gricushgr  48409  isubgr3stgrlem7  48464  uspgrlimlem4  48483  gpgedgvtx1  48554  pgn4cyclex  48618  uzlidlring  48727  2zrngmmgm  48744  cznrng  48753  ply1mulgsumlem2  48879  snlindsntor  48963  elbigo2  49044  nn0sumshdiglemA  49111  precofvalALT  49859