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  8050  ltmpi  10906  cshf1  14873  lcmfunsnlem  16723  mulgaddcom  19210  mulginvcom  19211  symgfvne  19497  voliunlem3  25764  3cyclfrgrrn  30710  numclwwlk1lem2foa  30778  frgrregord013  30819  strlem3a  32677  hstrlem3a  32685  chirredlem1  32815  nn0prpwlem  36892  matunitlindflem1  38326  zerdivemp1x  38658  athgt  40290  paddasslem14  40667  paddidm  40675  tendospcanN  41857  jm2.26  43789  relexpxpmin  44503  0ellimcdiv  46423  uhgrimisgrgric  48756  clnbgrgrimlem  48758