Theorem ad4ant14 752

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 715	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 715	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:  ad5ant15  759  ad5ant25  762  soisoi  7115  dfac9  9715  lediv12a  11690  leexp1a  13710  seqcoll  13995  lo1bdd2  15050  rlimcld2  15104  rlimcn1  15114  isercolllem1  15193  summo  15246  climcnds  15378  geomulcvg  15403  mertenslem2  15412  prodmolem2  15460  prodmo  15461  fprod2d  15506  pwsle  16951  isacs2  17110  grprinvlem  18099  gsumpropd2lem  18105  gsumwsubmcl  18217  gsumwmhm  18226  mulgfval  18444  gaid  18647  gsmsymgrfixlem1  18773  mulgnn0di  19165  gsumval3  19246  fvmptnn04if  21700  cnpnei  22115  lfinun  22376  xkopt  22506  isr0  22588  fbflim  22827  alexsubALTlem3  22900  metss  23360  iscmet3lem2  24143  ovoliunlem3  24355  mbfposr  24503  i1fmulclem  24554  itg10a  24562  iblss  24656  dvlip  24844  plyeq0lem  25058  mtest  25250  itgulm  25254  dchrisumlem3  26326  rpvmasum2  26347  pntlem3  26444  hlpasch  26801  f1otrg  26916  lfgrwlkprop  27729  wlkiswwlks1  27905  frgrnbnb  28330  frgr2wwlkeqm  28368  unidifsnne  30557  hashxpe  30801  ccatf1  30897  signstfvneq0  32217  bnj605  32554  nosupbday  33594  noinfbday  33609  matunitlindflem1  35459  matunitlindflem2  35460  poimirlem26  35489  mblfinlem2  35501  ssfiunibd  42462  xralrple2  42507  infleinf  42525  infxrpnf  42601  fprodcn  42759  limsupub  42863  limsuppnflem  42869  limsupmnflem  42879  cnrefiisplem  42988  climxlim2lem  43004  icccncfext  43046  cncficcgt0  43047  cncfioobd  43056  dvbdfbdioolem2  43088  itgspltprt  43138  stoweidlem34  43193  stoweidlem49  43208  stoweidlem57  43216  fourierdlem34  43300  fourierdlem39  43305  fourierdlem50  43315  fourierdlem51  43316  fourierdlem64  43329  fourierdlem73  43338  fourierdlem77  43342  fourierdlem81  43346  fourierdlem94  43359  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  fourierdlem113  43378  fourier2  43386  etransclem24  43417  intsal  43487  sge0pr  43550  sge0iunmptlemfi  43569  sge0seq  43602  sge0reuz  43603  nnfoctbdjlem  43611  meadjiunlem  43621  ismeannd  43623  carageniuncllem2  43678  isomennd  43687  hoicvr  43704  hspmbllem2  43783  iunhoiioolem  43831  iunhoiioo  43832  vonioo  43838  vonicc  43841  preimageiingt  43872  preimaleiinlt  43873  smfaddlem1  43913  smfaddlem2  43914  smflimlem4  43924  smfrec  43938  smfinflem  43965  sprsymrelf1lem  44559  lighneallem3  44675  isomgreqve  44893  1arymaptfo  45605