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  9583  cshf1  13356  lcmfunsnlem  15141  mulginvcom  17337  symgfvne  17580  voliunlem3  23072  frgraregord013  26439  strlem3a  28289  hstrlem3a  28297  chirredlem1  28427  nn0prpwlem  31281  matunitlindflem1  32369  zerdivemp1x  32710  athgt  33554  paddasslem14  33931  paddidm  33939  tendospcanN  35124  jm2.26  36381  relexpxpmin  36822  0ellimcdiv  38510  3cyclfrgrrn  41448  av-frgraregord013  41541