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  8045  ltmpi  10916  cshf1  14884  lcmfunsnlem  16734  mulgaddcom  19224  mulginvcom  19225  symgfvne  19511  matunitlindflem1  22904  voliunlem3  25783  3cyclfrgrrn  30769  numclwwlk1lem2foa  30837  frgrregord013  30878  strlem3a  32736  hstrlem3a  32744  chirredlem1  32874  nn0prpwlem  36944  zerdivemp1x  38700  athgt  40332  paddasslem14  40709  paddidm  40717  tendospcanN  41899  jm2.26  43846  relexpxpmin  44560  0ellimcdiv  46480  uhgrimisgrgric  48850  clnbgrgrimlem  48852