Theorem ad4ant14 1285

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis

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

Assertion

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

Proof of Theorem ad4ant14

Step	Hyp	Ref	Expression
1		ad4ant14.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 449	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	2a1d 26	. 2 ⊢ (𝜑 → (𝜃 → (𝜏 → (𝜓 → 𝜒))))
4	3	imp41 617	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pntlem3  25098  hlpasch  25448  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem26  32605  mblfinlem2  32617  ssfiunibd  38464  xralrple2  38511  infleinf  38529  fprodcn  38667  icccncfext  38773  cncficcgt0  38774  cncfioobd  38783  dvbdfbdioolem2  38819  itgspltprt  38871  stoweidlem34  38927  stoweidlem49  38942  stoweidlem57  38950  fourierdlem34  39034  fourierdlem39  39039  fourierdlem50  39049  fourierdlem51  39050  fourierdlem64  39063  fourierdlem73  39072  fourierdlem77  39076  fourierdlem81  39080  fourierdlem94  39093  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  fourier2  39120  etransclem24  39151  intsal  39224  sge0pr  39287  sge0iunmptlemfi  39306  sge0seq  39339  sge0reuz  39340  nnfoctbdjlem  39348  meadjiunlem  39358  ismeannd  39360  carageniuncllem2  39412  isomennd  39421  hoicvr  39438  hspmbllem2  39517  iunhoiioolem  39566  iunhoiioo  39567  vonioo  39573  vonicc  39576  preimageiingt  39607  preimaleiinlt  39608  smfaddlem1  39649  smfaddlem2  39650  smflimlem4  39660  smfrec  39674  lighneallem3  40062  lfgrwlkprop  40896  1wlkiswwlks1  41064  frgrnbnb  41463  frgrwopreglem5  41485