Theorem 3exp1 1414

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3an1rs  1421  ltmpi  10063  cshf1  13967  lcmfunsnlem  15770  mulgaddcom  17961  mulginvcom  17962  symgfvne  18202  voliunlem3  23767  3cyclfrgrrn  27711  numclwwlk1lem2foa  27786  numclwwlk1lem2foaOLD  27787  frgrregord013  27844  strlem3a  29700  hstrlem3a  29708  chirredlem1  29838  nn0prpwlem  32913  matunitlindflem1  34040  zerdivemp1x  34379  athgt  35619  paddasslem14  35996  paddidm  36004  tendospcanN  37186  jm2.26  38542  relexpxpmin  38980  0ellimcdiv  40803