Theorem 3exp1 1369

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3an1rs  1376  funelss  8044  ltmpi  10889  cshf1  14847  lcmfunsnlem  16699  mulgaddcom  19164  mulginvcom  19165  symgfvne  19451  voliunlem3  25680  3cyclfrgrrn  30578  numclwwlk1lem2foa  30646  frgrregord013  30687  strlem3a  32545  hstrlem3a  32553  chirredlem1  32683  nn0prpwlem  36722  matunitlindflem1  38155  zerdivemp1x  38486  athgt  40120  paddasslem14  40497  paddidm  40505  tendospcanN  41687  jm2.26  43621  relexpxpmin  44335  0ellimcdiv  46255  uhgrimisgrgric  48585  clnbgrgrimlem  48587