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

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

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  5146  fimaproj  8121  tfrlem1  8376  oaass  8561  undomOLD  9060  acndom2  10049  infxp  10210  isf32lem2  10349  ttukeylem3  10506  gchina  10694  r1limwun  10731  difreicc  13461  ssfzo12bi  13727  flflp1  13772  hasheqf1oi  14311  ccatcl  14524  cshwidxmodr  14754  wwlktovf1  14908  o1of2  15557  rlimsqzlem  15595  lcmgcdlem  16543  isprm5  16644  ramval  16941  mreexexlem4d  17591  acsfn  17603  gsumpropd2lem  18598  gasubg  19166  psgndiflemB  21153  psgndiflemA  21154  psrass1  21525  mdetf  22097  cpmatacl  22218  cpmatinvcl  22219  mat2pmatf1  22231  mp2pm2mplem4  22311  chfacffsupp  22358  restcld  22676  cnpnei  22768  iscncl  22773  cncls  22778  cnntr  22779  1stcfb  22949  2ndcdisj  22960  txlly  23140  fbflim  23480  fclsbas  23525  nmoi  24245  fgcfil  24788  equivcau  24817  cmetcusp  24871  itg2cnlem1  25279  iblss  25322  lgsqr  26854  lgsqrmodndvds  26856  noetainflem4  27243  slerec  27320  axcontlem2  28223  nbuhgr  28600  nbusgrvtxm1  28636  2pthon3v  29197  clwwisshclwwslem  29267  wwlksext2clwwlk  29310  2pthfrgr  29537  vdgn1frgrv2  29549  frgrwopreg  29576  numclwlk2lem2f1o  29632  blocnilem  30057  mdslmd3i  31585  foresf1o  31742  2ndresdju  31874  fgreu  31897  fdifsuppconst  31911  resf1o  31955  omndmul2  32230  psgnfzto1st  32264  isdrng4  32395  nsgqusf1olem3  32526  elrspunidl  32546  elrspunsn  32547  qsidomlem1  32571  lbsdiflsp0  32711  ist0cld  32813  locfinreflem  32820  cmpcref  32830  zarclsun  32850  pstmxmet  32877  lmdvg  32933  carsgclctunlem3  33319  oddpwdc  33353  sgnmul  33541  signstres  33586  tgoldbachgtd  33674  cvmlift2lem12  34305  satfdmlem  34359  satffunlem2lem1  34395  mrsubff  34503  mpomulcn  35162  elicc3  35202  nn0prpwlem  35207  neibastop2  35246  neibastop3  35247  bj-prmoore  35996  ltflcei  36476  matunitlindflem2  36485  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  heicant  36523  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  nnubfi  36618  nninfnub  36619  linepsubN  38623  lhpmatb  38902  cdlemf2  39433  diaglbN  39926  diaintclN  39929  dibglbN  40037  dibintclN  40038  dihlsscpre  40105  dihglblem5aN  40163  dihglblem2aN  40164  dih1dimatlem  40200  sticksstones12a  40973  fsuppind  41162  diophren  41551  irrapxlem2  41561  irrapxlem4  41563  wepwsolem  41784  omlimcl2  41991  tfsconcatfv  42091  ofoafg  42104  prmunb2  43070  cvgdvgrat  43072  fiiuncl  43752  infleinflem2  44081  supxrunb3  44109  supminfxr  44174  limsuppnflem  44426  limsupmnflem  44436  limsupre3lem  44448  dfxlim2v  44563  icccncfext  44603  ioodvbdlimc1lem1  44647  iblcncfioo  44694  wallispilem3  44783  fourierdlem12  44835  fourierdlem34  44857  fourierdlem50  44872  fourierdlem51  44873  fourierdlem65  44887  fourierdlem77  44899  meaiuninc3v  45200  hoicvr  45264  hspdifhsp  45332  smflimlem4  45490  iccpartigtl  46091  iccpartgt  46095  fargshiftfva  46111  sfprmdvdsmersenne  46271  opoeALTV  46351  opeoALTV  46352  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  isomushgr  46494  isomuspgr  46502  issubmgm2  46560  uzlidlring  46827  2zrngmmgm  46844  cznrng  46853  ply1mulgsumlem2  47068  snlindsntor  47152  elbigo2  47238  nn0sumshdiglemA  47305