Theorem ad4ant14 765

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
ad4ant14	⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 728	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 728	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad5ant15  771  ad5ant25  774  ad5ant125  1391  soisoi  7367  dfac9  10254  lediv12a  12250  leexp1a  14358  seqcoll  14650  ccatf1  14777  lo1bdd2  15735  rlimcld2  15789  rlimcn1  15799  isercolllem1  15876  summo  15927  climcnds  16064  geomulcvg  16089  mertenslem2  16098  prodmolem2  16146  prodmo  16147  fprod2d  16192  pwsle  17714  isacs2  17877  grpinvalem  18904  gsumpropd2lem  18918  gsumwsubmcl  19083  gsumwmhm  19091  mulgfval  19329  gaid  19564  gsmsymgrfixlem1  19692  mulgnn0di  20090  gsumval3  20172  subrngint  20863  matunitlindflem1  23049  matunitlindflem2  23050  fvmptnn04if  23222  cnpnei  23637  lfinun  23899  xkopt  24029  isr0  24111  fbflim  24350  alexsubALTlem3  24423  metss  24882  iscmet3lem2  25668  ovoliunlem3  25880  mbfposr  26028  i1fmulclem  26078  itg10a  26086  iblss  26180  dvlip  26368  plyeq0lem  26584  mtest  26788  itgulm  26792  dchrisumlem3  27875  rpvmasum2  27896  pntlem3  27993  nosupbday  28119  noinfbday  28134  addonbday  28722  hlpasch  29291  f1otrg  29505  lfgrwlkprop  30327  wlkiswwlks1  30513  frgrnbnb  30951  frgr2wwlkeqm  30989  unidifsnne  33230  hashxpe  33495  fxpsubm  33832  fxpsubrg  33834  mplvrpmmhm  34289  mplvrpmrhm  34290  esplyfval1  34316  vieta  34323  cos9thpiminplylem1  34525  omssubadd  35043  signstfvneq0  35312  bnj605  35648  poimirlem26  38832  mblfinlem2  38844  ssfiunibd  46598  xralrple2  46639  infleinf  46656  infxrpnf  46729  fprodcn  46885  limsupub  46987  limsuppnflem  46993  limsupmnflem  47003  cnrefiisplem  47112  climxlim2lem  47128  icccncfext  47170  cncficcgt0  47171  cncfioobd  47180  dvbdfbdioolem2  47212  dvmptfprod  47228  itgspltprt  47262  stoweidlem34  47317  stoweidlem49  47332  stoweidlem57  47340  fourierdlem34  47424  fourierdlem39  47429  fourierdlem50  47439  fourierdlem51  47440  fourierdlem64  47453  fourierdlem73  47462  fourierdlem77  47466  fourierdlem81  47470  fourierdlem94  47483  fourierdlem97  47486  fourierdlem103  47492  fourierdlem104  47493  fourierdlem113  47502  fourier2  47510  etransclem24  47541  intsal  47613  sge0pr  47677  sge0iunmptlemfi  47696  sge0seq  47729  sge0reuz  47730  nnfoctbdjlem  47738  meadjiunlem  47748  ismeannd  47750  carageniuncllem2  47805  isomennd  47814  hoicvr  47831  hspmbllem2  47910  iunhoiioolem  47958  iunhoiioo  47959  vonioo  47965  vonicc  47968  preimageiingt  48003  preimaleiinlt  48004  smfaddlem1  48046  smfaddlem2  48047  smflimlem4  48057  smfrec  48072  smfinflem  48100  sprsymrelf1lem  48846  lighneallem3  48965  1arymaptfo  50086