Theorem ad3antlr 731

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simpllr  776  disjxiun  5027  fimaproj  7855  tfrlem1  8041  oaass  8218  undom  8654  acndom2  9554  infxp  9715  isf32lem2  9854  ttukeylem3  10011  gchina  10199  r1limwun  10236  difreicc  12958  ssfzo12bi  13223  flflp1  13268  hasheqf1oi  13804  ccatcl  14015  cshwidxmodr  14255  wwlktovf1  14410  o1of2  15060  rlimsqzlem  15098  lcmgcdlem  16047  isprm5  16148  ramval  16444  mreexexlem4d  17021  acsfn  17033  gsumpropd2lem  18005  gasubg  18550  psgndiflemB  20416  psgndiflemA  20417  mdetf  21346  cpmatacl  21467  cpmatinvcl  21468  mat2pmatf1  21480  mp2pm2mplem4  21560  chfacffsupp  21607  restcld  21923  cnpnei  22015  iscncl  22020  cncls  22025  cnntr  22026  1stcfb  22196  2ndcdisj  22207  txlly  22387  fbflim  22727  fclsbas  22772  nmoi  23481  fgcfil  24023  equivcau  24052  cmetcusp  24106  itg2cnlem1  24514  iblss  24557  lgsqr  26087  lgsqrmodndvds  26089  axcontlem2  26911  nbuhgr  27285  nbusgrvtxm1  27321  2pthon3v  27881  clwwisshclwwslem  27951  wwlksext2clwwlk  27994  2pthfrgr  28221  vdgn1frgrv2  28233  frgrwopreg  28260  numclwlk2lem2f1o  28316  blocnilem  28739  mdslmd3i  30267  foresf1o  30424  2ndresdju  30560  fgreu  30584  fdifsuppconst  30598  resf1o  30640  omndmul2  30915  psgnfzto1st  30949  nsgqusf1olem3  31172  elrspunidl  31178  qsidomlem1  31200  lbsdiflsp0  31279  ist0cld  31355  locfinreflem  31362  cmpcref  31372  zarclsun  31392  pstmxmet  31419  lmdvg  31475  carsgclctunlem3  31857  oddpwdc  31891  sgnmul  32079  signstres  32124  tgoldbachgtd  32212  cvmlift2lem12  32847  satfdmlem  32901  satffunlem2lem1  32937  mrsubff  33045  noetainflem4  33584  slerec  33654  elicc3  34144  nn0prpwlem  34149  neibastop2  34188  neibastop3  34189  bj-prmoore  34907  ltflcei  35388  matunitlindflem2  35397  poimirlem4  35404  poimirlem13  35413  poimirlem14  35414  poimirlem26  35426  poimirlem27  35427  poimirlem28  35428  poimirlem29  35429  poimirlem31  35431  heicant  35435  mblfinlem2  35438  mblfinlem3  35439  mblfinlem4  35440  ismblfin  35441  itg2addnclem  35451  itg2addnclem2  35452  itg2addnclem3  35453  itg2addnc  35454  itg2gt0cn  35455  ftc1cnnc  35472  ftc1anclem5  35477  ftc1anclem6  35478  ftc1anclem7  35479  ftc1anclem8  35480  ftc1anc  35481  nnubfi  35531  nninfnub  35532  linepsubN  37389  lhpmatb  37668  cdlemf2  38199  diaglbN  38692  diaintclN  38695  dibglbN  38803  dibintclN  38804  dihlsscpre  38871  dihglblem5aN  38929  dihglblem2aN  38930  dih1dimatlem  38966  fsuppind  39858  diophren  40207  irrapxlem2  40217  irrapxlem4  40219  wepwsolem  40439  prmunb2  41467  cvgdvgrat  41469  fiiuncl  42151  infleinflem2  42448  supxrunb3  42477  supminfxr  42544  limsuppnflem  42793  limsupmnflem  42803  limsupre3lem  42815  dfxlim2v  42930  icccncfext  42970  ioodvbdlimc1lem1  43014  iblcncfioo  43061  wallispilem3  43150  fourierdlem12  43202  fourierdlem34  43224  fourierdlem50  43239  fourierdlem51  43240  fourierdlem65  43254  fourierdlem77  43266  meaiuninc3v  43564  hoicvr  43628  hspdifhsp  43696  smflimlem4  43848  iccpartigtl  44409  iccpartgt  44413  fargshiftfva  44429  sfprmdvdsmersenne  44589  opoeALTV  44669  opeoALTV  44670  nnsum4primeseven  44786  nnsum4primesevenALTV  44787  isomushgr  44812  isomuspgr  44820  issubmgm2  44878  uzlidlring  45021  2zrngmmgm  45038  cznrng  45047  ply1mulgsumlem2  45262  snlindsntor  45346  elbigo2  45432  nn0sumshdiglemA  45499