Theorem 3exp1 1353

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3an1rs  1360  funelss  7991  ltmpi  10815  cshf1  14733  lcmfunsnlem  16568  mulgaddcom  19028  mulginvcom  19029  symgfvne  19310  voliunlem3  25509  3cyclfrgrrn  30361  numclwwlk1lem2foa  30429  frgrregord013  30470  strlem3a  32327  hstrlem3a  32335  chirredlem1  32465  nn0prpwlem  36516  matunitlindflem1  37817  zerdivemp1x  38148  athgt  39726  paddasslem14  40103  paddidm  40111  tendospcanN  41293  jm2.26  43254  relexpxpmin  43968  0ellimcdiv  45903  uhgrimisgrgric  48187  clnbgrgrimlem  48189