Theorem 3exp1 1283

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  ltmpi  9726  cshf1  13556  lcmfunsnlem  15354  mulginvcom  17565  symgfvne  17808  voliunlem3  23320  3cyclfrgrrn  27150  frgrregord013  27253  strlem3a  29111  hstrlem3a  29119  chirredlem1  29249  nn0prpwlem  32317  matunitlindflem1  33405  zerdivemp1x  33746  athgt  34742  paddasslem14  35119  paddidm  35127  tendospcanN  36312  jm2.26  37569  relexpxpmin  38009  0ellimcdiv  39881