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  5107  fimaproj  8117  tfrlem1  8347  oaass  8528  undomOLD  9034  acndom2  10014  infxp  10174  isf32lem2  10314  ttukeylem3  10471  gchina  10659  r1limwun  10696  difreicc  13452  ssfzo12bi  13729  flflp1  13776  hasheqf1oi  14323  ccatcl  14546  cshwidxmodr  14776  wwlktovf1  14930  o1of2  15586  rlimsqzlem  15622  lcmgcdlem  16583  isprm5  16684  ramval  16986  mreexexlem4d  17615  acsfn  17627  gsumpropd2lem  18613  issubmgm2  18637  gasubg  19241  psgndiflemB  21516  psgndiflemA  21517  psrass1  21880  mhpmulcl  22043  mdetf  22489  cpmatacl  22610  cpmatinvcl  22611  mat2pmatf1  22623  mp2pm2mplem4  22703  chfacffsupp  22750  restcld  23066  cnpnei  23158  iscncl  23163  cncls  23168  cnntr  23169  1stcfb  23339  2ndcdisj  23350  txlly  23530  fbflim  23870  fclsbas  23915  nmoi  24623  mpomulcn  24765  fgcfil  25178  equivcau  25207  cmetcusp  25261  itg2cnlem1  25669  iblss  25713  lgsqr  27269  lgsqrmodndvds  27271  noetainflem4  27659  slerec  27738  remulscllem2  28359  axcontlem2  28899  nbuhgr  29277  nbusgrvtxm1  29313  2pthon3v  29880  clwwisshclwwslem  29950  wwlksext2clwwlk  29993  2pthfrgr  30220  vdgn1frgrv2  30232  frgrwopreg  30259  numclwlk2lem2f1o  30315  blocnilem  30740  mdslmd3i  32268  foresf1o  32440  2ndresdju  32580  fgreu  32603  fdifsuppconst  32619  resf1o  32660  sgnmul  32767  chnso  32947  omndmul2  33033  psgnfzto1st  33069  elrgspnsubrunlem1  33205  isdrng4  33252  nsgqusf1olem3  33393  elrspunidl  33406  elrspunsn  33407  qsidomlem1  33430  1arithidom  33515  dfufd2lem  33527  lbsdiflsp0  33629  evls1fldgencl  33672  cos9thpiminplylem2  33780  ist0cld  33830  locfinreflem  33837  cmpcref  33847  zarclsun  33867  pstmxmet  33894  lmdvg  33950  carsgclctunlem3  34318  oddpwdc  34352  signstres  34573  tgoldbachgtd  34660  cvmlift2lem12  35308  satfdmlem  35362  satffunlem2lem1  35398  mrsubff  35506  elicc3  36312  nn0prpwlem  36317  neibastop2  36356  neibastop3  36357  bj-prmoore  37110  ltflcei  37609  matunitlindflem2  37618  poimirlem4  37625  poimirlem13  37634  poimirlem14  37635  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  nnubfi  37751  nninfnub  37752  linepsubN  39753  lhpmatb  40032  cdlemf2  40563  diaglbN  41056  diaintclN  41059  dibglbN  41167  dibintclN  41168  dihlsscpre  41235  dihglblem5aN  41293  dihglblem2aN  41294  dih1dimatlem  41330  sticksstones12a  42152  fsuppind  42585  diophren  42808  irrapxlem2  42818  irrapxlem4  42820  wepwsolem  43038  omlimcl2  43238  tfsconcatfv  43337  ofoafg  43350  prmunb2  44307  cvgdvgrat  44309  fiiuncl  45066  infleinflem2  45374  supxrunb3  45402  supminfxr  45467  limsuppnflem  45715  limsupmnflem  45725  limsupre3lem  45737  dfxlim2v  45852  icccncfext  45892  ioodvbdlimc1lem1  45936  iblcncfioo  45983  wallispilem3  46072  fourierdlem12  46124  fourierdlem34  46146  fourierdlem50  46161  fourierdlem51  46162  fourierdlem65  46176  fourierdlem77  46188  meaiuninc3v  46489  hoicvr  46553  hspdifhsp  46621  smflimlem4  46779  iccpartigtl  47428  iccpartgt  47432  fargshiftfva  47448  sfprmdvdsmersenne  47608  opoeALTV  47688  opeoALTV  47689  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  uhgrimedgi  47894  isuspgrimlem  47899  gricushgr  47921  isubgr3stgrlem7  47975  uspgrlimlem4  47994  gpgedgvtx1  48057  pgn4cyclex  48120  uzlidlring  48227  2zrngmmgm  48244  cznrng  48253  ply1mulgsumlem2  48380  snlindsntor  48464  elbigo2  48545  nn0sumshdiglemA  48612  precofvalALT  49361