Theorem 3exp1 1275

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ltmpi  9605  cshf1  13407  lcmfunsnlem  15192  mulginvcom  17388  symgfvne  17631  voliunlem3  23127  frgraregord013  26645  strlem3a  28495  hstrlem3a  28503  chirredlem1  28633  nn0prpwlem  31487  matunitlindflem1  32575  zerdivemp1x  32916  athgt  33760  paddasslem14  34137  paddidm  34145  tendospcanN  35330  jm2.26  36587  relexpxpmin  37028  0ellimcdiv  38716  3cyclfrgrrn  41456  av-frgraregord013  41549