Theorem 3exp1 1354

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 1120	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3an1rs  1361  funelss  8000  ltmpi  10827  cshf1  14772  lcmfunsnlem  16610  mulgaddcom  19074  mulginvcom  19075  symgfvne  19356  voliunlem3  25519  3cyclfrgrrn  30356  numclwwlk1lem2foa  30424  frgrregord013  30465  strlem3a  32323  hstrlem3a  32331  chirredlem1  32461  nn0prpwlem  36504  matunitlindflem1  37937  zerdivemp1x  38268  athgt  39902  paddasslem14  40279  paddidm  40287  tendospcanN  41469  jm2.26  43430  relexpxpmin  44144  0ellimcdiv  46077  uhgrimisgrgric  48407  clnbgrgrimlem  48409