Theorem 3exp1 1352

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  3an1rs  1359  funelss  8035  ltmpi  10901  cshf1  14764  lcmfunsnlem  16582  mulgaddcom  19014  mulginvcom  19015  symgfvne  19289  voliunlem3  25293  3cyclfrgrrn  29794  numclwwlk1lem2foa  29862  frgrregord013  29903  strlem3a  31760  hstrlem3a  31768  chirredlem1  31898  nn0prpwlem  35510  matunitlindflem1  36787  zerdivemp1x  37118  athgt  38630  paddasslem14  39007  paddidm  39015  tendospcanN  40197  jm2.26  42043  relexpxpmin  42770  0ellimcdiv  44664