Theorem 3exp1 1305

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3an1rs  1312  ltmpi  9764  cshf1  13602  lcmfunsnlem  15401  mulginvcom  17612  symgfvne  17854  voliunlem3  23366  3cyclfrgrrn  27266  numclwlk1lem2foa  27344  frgrregord013  27382  strlem3a  29239  hstrlem3a  29247  chirredlem1  29377  nn0prpwlem  32442  matunitlindflem1  33535  zerdivemp1x  33876  athgt  35060  paddasslem14  35437  paddidm  35445  tendospcanN  36629  jm2.26  37886  relexpxpmin  38326  0ellimcdiv  40199