Theorem 3exp1 1366

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3an1rs  1373  funelss  8028  ltmpi  10862  cshf1  14823  lcmfunsnlem  16675  mulgaddcom  19140  mulginvcom  19141  symgfvne  19421  voliunlem3  25614  3cyclfrgrrn  30488  numclwwlk1lem2foa  30556  frgrregord013  30597  strlem3a  32455  hstrlem3a  32463  chirredlem1  32593  nn0prpwlem  36682  matunitlindflem1  38115  zerdivemp1x  38446  athgt  40080  paddasslem14  40457  paddidm  40465  tendospcanN  41647  jm2.26  43579  relexpxpmin  44293  0ellimcdiv  46223  uhgrimisgrgric  48553  clnbgrgrimlem  48555