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

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

This theorem is referenced by:  3an1rs  1359  funelss  8088  ltmpi  10973  cshf1  14858  lcmfunsnlem  16688  mulgaddcom  19138  mulginvcom  19139  symgfvne  19422  voliunlem3  25606  3cyclfrgrrn  30318  numclwwlk1lem2foa  30386  frgrregord013  30427  strlem3a  32284  hstrlem3a  32292  chirredlem1  32422  nn0prpwlem  36288  matunitlindflem1  37576  zerdivemp1x  37907  athgt  39413  paddasslem14  39790  paddidm  39798  tendospcanN  40980  jm2.26  42959  relexpxpmin  43679  0ellimcdiv  45570  uhgrimisgrgric  47783  clnbgrgrimlem  47785