Theorem 3exp1 1371

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3an1rs  1378  funelss  8058  ltmpi  10989  cshf1  14961  lcmfunsnlem  16816  mulgaddcom  19308  mulginvcom  19309  symgfvne  19595  matunitlindflem1  22994  voliunlem3  25873  3cyclfrgrrn  30887  numclwwlk1lem2foa  30955  frgrregord013  30996  strlem3a  32854  hstrlem3a  32862  chirredlem1  32992  nn0prpwlem  37110  zerdivemp1x  38881  athgt  40513  paddasslem14  40890  paddidm  40898  tendospcanN  42080  jm2.26  44008  relexpxpmin  44716  0ellimcdiv  46658  uhgrimisgrgric  49028  clnbgrgrimlem  49030