Theorem 3exp1 1351

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  3an1rs  1358  funelss  7882  ltmpi  10671  cshf1  14534  lcmfunsnlem  16357  mulgaddcom  18738  mulginvcom  18739  symgfvne  18999  voliunlem3  24727  3cyclfrgrrn  28659  numclwwlk1lem2foa  28727  frgrregord013  28768  strlem3a  30623  hstrlem3a  30631  chirredlem1  30761  nn0prpwlem  34520  matunitlindflem1  35782  zerdivemp1x  36114  athgt  37479  paddasslem14  37856  paddidm  37864  tendospcanN  39046  jm2.26  40833  relexpxpmin  41307  0ellimcdiv  43172