Theorem 3exp1 1371

Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Hypothesis

Ref	Expression
3exp1.1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
3exp1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem 3exp1

Step	Hyp	Ref	Expression
1		3exp1.1	. . 3 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
2	1	ex 417	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	3exp 1137	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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  df-3an 1105

This theorem is referenced by:  3an1rs  1378  funelss  8040  ltmpi  10884  cshf1  14843  lcmfunsnlem  16694  mulgaddcom  19159  mulginvcom  19160  symgfvne  19446  voliunlem3  25711  3cyclfrgrrn  30637  numclwwlk1lem2foa  30705  frgrregord013  30746  strlem3a  32604  hstrlem3a  32612  chirredlem1  32742  nn0prpwlem  36853  matunitlindflem1  38287  zerdivemp1x  38618  athgt  40250  paddasslem14  40627  paddidm  40635  tendospcanN  41817  jm2.26  43749  relexpxpmin  44463  0ellimcdiv  46383  uhgrimisgrgric  48716  clnbgrgrimlem  48718