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

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 398  df-3an 1089

This theorem is referenced by:  3an1rs  1359  funelss  7920  ltmpi  10706  cshf1  14568  lcmfunsnlem  16391  mulgaddcom  18772  mulginvcom  18773  symgfvne  19033  voliunlem3  24761  3cyclfrgrrn  28695  numclwwlk1lem2foa  28763  frgrregord013  28804  strlem3a  30659  hstrlem3a  30667  chirredlem1  30797  nn0prpwlem  34556  matunitlindflem1  35817  zerdivemp1x  36149  athgt  37512  paddasslem14  37889  paddidm  37897  tendospcanN  39079  jm2.26  40862  relexpxpmin  41363  0ellimcdiv  43239