Theorem 3exp1 1349

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3an1rs  1356  funelss  7728  ltmpi  10315  cshf1  14163  lcmfunsnlem  15975  mulgaddcom  18243  mulginvcom  18244  symgfvne  18501  voliunlem3  24156  3cyclfrgrrn  28071  numclwwlk1lem2foa  28139  frgrregord013  28180  strlem3a  30035  hstrlem3a  30043  chirredlem1  30173  nn0prpwlem  33783  matunitlindflem1  35053  zerdivemp1x  35385  athgt  36752  paddasslem14  37129  paddidm  37137  tendospcanN  38319  jm2.26  39943  relexpxpmin  40418  0ellimcdiv  42291