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 418	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
3	2	3exp 1137	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

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

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

This theorem is used by:  3an1rs  1378  funelss  8069  ltmpi  11002  cshf1  14975  lcmfunsnlem  16831  mulgaddcom  19323  mulginvcom  19324  symgfvne  19610  matunitlindflem1  23009  voliunlem3  25888  3cyclfrgrrn  30902  numclwwlk1lem2foa  30970  frgrregord013  31011  strlem3a  32869  hstrlem3a  32877  chirredlem1  33007  nn0prpwlem  37240  zerdivemp1x  39024  athgt  40656  paddasslem14  41033  paddidm  41041  tendospcanN  42223  jm2.26  44152  relexpxpmin  44860  0ellimcdiv  46801  uhgrimisgrgric  49171  clnbgrgrimlem  49173