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  8029  ltmpi  10895  cshf1  14756  lcmfunsnlem  16574  mulgaddcom  18972  mulginvcom  18973  symgfvne  19242  voliunlem3  25060  3cyclfrgrrn  29528  numclwwlk1lem2foa  29596  frgrregord013  29637  strlem3a  31492  hstrlem3a  31500  chirredlem1  31630  nn0prpwlem  35195  matunitlindflem1  36472  zerdivemp1x  36803  athgt  38315  paddasslem14  38692  paddidm  38700  tendospcanN  39882  jm2.26  41726  relexpxpmin  42453  0ellimcdiv  44351