Theorem 3exp1 1348

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3an1rs  1355  funelss  7749  ltmpi  10329  cshf1  14175  lcmfunsnlem  15988  mulgaddcom  18254  mulginvcom  18255  symgfvne  18512  voliunlem3  24156  3cyclfrgrrn  28068  numclwwlk1lem2foa  28136  frgrregord013  28177  strlem3a  30032  hstrlem3a  30040  chirredlem1  30170  nn0prpwlem  33674  matunitlindflem1  34892  zerdivemp1x  35229  athgt  36596  paddasslem14  36973  paddidm  36981  tendospcanN  38163  jm2.26  39605  relexpxpmin  40068  0ellimcdiv  41936