Theorem ad4ant14 748

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 711	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantlr 711	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 206  df-an 396

This theorem is referenced by:  ad5ant15  755  ad5ant25  758  soisoi  7179  dfac9  9823  lediv12a  11798  leexp1a  13821  seqcoll  14106  lo1bdd2  15161  rlimcld2  15215  rlimcn1  15225  isercolllem1  15304  summo  15357  climcnds  15491  geomulcvg  15516  mertenslem2  15525  prodmolem2  15573  prodmo  15574  fprod2d  15619  pwsle  17120  isacs2  17279  grprinvlem  18272  gsumpropd2lem  18278  gsumwsubmcl  18390  gsumwmhm  18399  mulgfval  18617  gaid  18820  gsmsymgrfixlem1  18950  mulgnn0di  19342  gsumval3  19423  fvmptnn04if  21906  cnpnei  22323  lfinun  22584  xkopt  22714  isr0  22796  fbflim  23035  alexsubALTlem3  23108  metss  23570  iscmet3lem2  24361  ovoliunlem3  24573  mbfposr  24721  i1fmulclem  24772  itg10a  24780  iblss  24874  dvlip  25062  plyeq0lem  25276  mtest  25468  itgulm  25472  dchrisumlem3  26544  rpvmasum2  26565  pntlem3  26662  hlpasch  27021  f1otrg  27136  lfgrwlkprop  27957  wlkiswwlks1  28133  frgrnbnb  28558  frgr2wwlkeqm  28596  unidifsnne  30785  hashxpe  31029  ccatf1  31125  signstfvneq0  32451  bnj605  32787  nosupbday  33835  noinfbday  33850  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem26  35730  mblfinlem2  35742  ssfiunibd  42738  xralrple2  42783  infleinf  42801  infxrpnf  42876  fprodcn  43031  limsupub  43135  limsuppnflem  43141  limsupmnflem  43151  cnrefiisplem  43260  climxlim2lem  43276  icccncfext  43318  cncficcgt0  43319  cncfioobd  43328  dvbdfbdioolem2  43360  itgspltprt  43410  stoweidlem34  43465  stoweidlem49  43480  stoweidlem57  43488  fourierdlem34  43572  fourierdlem39  43577  fourierdlem50  43587  fourierdlem51  43588  fourierdlem64  43601  fourierdlem73  43610  fourierdlem77  43614  fourierdlem81  43618  fourierdlem94  43631  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  fourier2  43658  etransclem24  43689  intsal  43759  sge0pr  43822  sge0iunmptlemfi  43841  sge0seq  43874  sge0reuz  43875  nnfoctbdjlem  43883  meadjiunlem  43893  ismeannd  43895  carageniuncllem2  43950  isomennd  43959  hoicvr  43976  hspmbllem2  44055  iunhoiioolem  44103  iunhoiioo  44104  vonioo  44110  vonicc  44113  preimageiingt  44144  preimaleiinlt  44145  smfaddlem1  44185  smfaddlem2  44186  smflimlem4  44196  smfrec  44210  smfinflem  44237  sprsymrelf1lem  44831  lighneallem3  44947  isomgreqve  45165  1arymaptfo  45877