Theorem 3exp1 1350

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 1117	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3an1rs  1357  funelss  7874  ltmpi  10644  cshf1  14504  lcmfunsnlem  16327  mulgaddcom  18708  mulginvcom  18709  symgfvne  18969  voliunlem3  24697  3cyclfrgrrn  28629  numclwwlk1lem2foa  28697  frgrregord013  28738  strlem3a  30593  hstrlem3a  30601  chirredlem1  30731  nn0prpwlem  34490  matunitlindflem1  35752  zerdivemp1x  36084  athgt  37449  paddasslem14  37826  paddidm  37834  tendospcanN  39016  jm2.26  40804  relexpxpmin  41278  0ellimcdiv  43144