Theorem ad4ant13 763

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad4ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad4ant13	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 485	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 731	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  ad5ant14  769  ad5ant24  772  ad5ant124  1386  fntpb  7208  peano5  7889  f1o2ndf1  8116  cantnfle  9639  cantnflem1c  9655  ttukeylem5  10496  rlimsqzlem  15699  dvdslcmf  16688  poslubmo  18464  posglbmo  18465  smndex1mgm  18968  isgrpinv  19059  ghmgrp  19131  dprdfcntz  20086  pzriprnglem4  21602  sraassab  21986  cply1coe0bi  22430  evls1fpws  22497  isnrm3  23484  cnextcn  24192  ustexsym  24341  ustex2sym  24342  ustex3sym  24343  trust  24354  fmucnd  24416  trcfilu  24418  metust  24683  cxpmul2z  26821  umgrres1lem  29600  upgrres1  29603  friendshipgt3  30689  ccatf1  33209  cyc3evpm  33410  elrgspnlem1  33502  elrgspnlem2  33503  elrgspnlem4  33505  elrgspnsubrunlem1  33507  elrgspnsubrunlem2  33508  znfermltl  33623  rhmimaidl  33683  selvply1rhmlema  33852  evlextv  33876  dimlssid  33966  txomap  34168  zart0  34213  repr0  34942  breprexplemc  34963  hgt750lemb  34987  satffunlem1lem2  35793  satffunlem2lem2  35796  lindsadd  38151  matunitlindflem1  38154  nadd1suc  44010  mapss2  45813  supxrge  45945  xrlexaddrp  45959  infxr  45973  infleinf  45978  unb2ltle  46020  supminfxr  46069  limsuppnfdlem  46306  limsupub  46309  limsuppnflem  46315  climinf3  46321  limsupmnflem  46325  climxrre  46355  liminfvalxr  46388  fperdvper  46524  sge0isum  47032  sge0gtfsumgt  47048  sge0seq  47051  nnfoctbdjlem  47060  meaiuninc3v  47089  omeiunltfirp  47124  hspdifhsp  47221  hspmbllem2  47232  pimdecfgtioo  47322  pimincfltioo  47323  preimageiingt  47325  preimaleiinlt  47326  smfid  47357  proththd  48254