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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simpllr  775  disjxiun  5104  fimaproj  8114  tfrlem1  8344  oaass  8525  acndom2  10007  infxp  10167  isf32lem2  10307  ttukeylem3  10464  gchina  10652  r1limwun  10689  difreicc  13445  ssfzo12bi  13722  flflp1  13769  hasheqf1oi  14316  ccatcl  14539  cshwidxmodr  14769  wwlktovf1  14923  o1of2  15579  rlimsqzlem  15615  lcmgcdlem  16576  isprm5  16677  ramval  16979  mreexexlem4d  17608  acsfn  17620  gsumpropd2lem  18606  issubmgm2  18630  gasubg  19234  psgndiflemB  21509  psgndiflemA  21510  psrass1  21873  mhpmulcl  22036  mdetf  22482  cpmatacl  22603  cpmatinvcl  22604  mat2pmatf1  22616  mp2pm2mplem4  22696  chfacffsupp  22743  restcld  23059  cnpnei  23151  iscncl  23156  cncls  23161  cnntr  23162  1stcfb  23332  2ndcdisj  23343  txlly  23523  fbflim  23863  fclsbas  23908  nmoi  24616  mpomulcn  24758  fgcfil  25171  equivcau  25200  cmetcusp  25254  itg2cnlem1  25662  iblss  25706  lgsqr  27262  lgsqrmodndvds  27264  noetainflem4  27652  slerec  27731  remulscllem2  28352  axcontlem2  28892  nbuhgr  29270  nbusgrvtxm1  29306  2pthon3v  29873  clwwisshclwwslem  29943  wwlksext2clwwlk  29986  2pthfrgr  30213  vdgn1frgrv2  30225  frgrwopreg  30252  numclwlk2lem2f1o  30308  blocnilem  30733  mdslmd3i  32261  foresf1o  32433  2ndresdju  32573  fgreu  32596  fdifsuppconst  32612  resf1o  32653  sgnmul  32760  chnso  32940  omndmul2  33026  psgnfzto1st  33062  elrgspnsubrunlem1  33198  isdrng4  33245  nsgqusf1olem3  33386  elrspunidl  33399  elrspunsn  33400  qsidomlem1  33423  1arithidom  33508  dfufd2lem  33520  lbsdiflsp0  33622  evls1fldgencl  33665  cos9thpiminplylem2  33773  ist0cld  33823  locfinreflem  33830  cmpcref  33840  zarclsun  33860  pstmxmet  33887  lmdvg  33943  carsgclctunlem3  34311  oddpwdc  34345  signstres  34566  tgoldbachgtd  34653  cvmlift2lem12  35301  satfdmlem  35355  satffunlem2lem1  35391  mrsubff  35499  elicc3  36305  nn0prpwlem  36310  neibastop2  36349  neibastop3  36350  bj-prmoore  37103  ltflcei  37602  matunitlindflem2  37611  poimirlem4  37618  poimirlem13  37627  poimirlem14  37628  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  ftc1cnnc  37686  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  nnubfi  37744  nninfnub  37745  linepsubN  39746  lhpmatb  40025  cdlemf2  40556  diaglbN  41049  diaintclN  41052  dibglbN  41160  dibintclN  41161  dihlsscpre  41228  dihglblem5aN  41286  dihglblem2aN  41287  dih1dimatlem  41323  sticksstones12a  42145  fsuppind  42578  diophren  42801  irrapxlem2  42811  irrapxlem4  42813  wepwsolem  43031  omlimcl2  43231  tfsconcatfv  43330  ofoafg  43343  prmunb2  44300  cvgdvgrat  44302  fiiuncl  45059  infleinflem2  45367  supxrunb3  45395  supminfxr  45460  limsuppnflem  45708  limsupmnflem  45718  limsupre3lem  45730  dfxlim2v  45845  icccncfext  45885  ioodvbdlimc1lem1  45929  iblcncfioo  45976  wallispilem3  46065  fourierdlem12  46117  fourierdlem34  46139  fourierdlem50  46154  fourierdlem51  46155  fourierdlem65  46169  fourierdlem77  46181  meaiuninc3v  46482  hoicvr  46546  hspdifhsp  46614  smflimlem4  46772  iccpartigtl  47424  iccpartgt  47428  fargshiftfva  47444  sfprmdvdsmersenne  47604  opoeALTV  47684  opeoALTV  47685  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  uhgrimedgi  47890  isuspgrimlem  47895  gricushgr  47917  isubgr3stgrlem7  47971  uspgrlimlem4  47990  gpgedgvtx1  48053  pgn4cyclex  48116  uzlidlring  48223  2zrngmmgm  48240  cznrng  48249  ply1mulgsumlem2  48376  snlindsntor  48460  elbigo2  48541  nn0sumshdiglemA  48608  precofvalALT  49357