Theorem 3impib 1179

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1175	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mob  2861  eqreu  2871  funimaexglem  5201  ssimaexg  5476  rbropap  6133  dfsmo2  6177  3ecoptocl  6511  distrnq0  7260  addassnq0  7263  uzind  9155  fzind  9159  fnn0ind  9160  xltnegi  9611  facwordi  10479  shftvalg  10601  shftval4g  10602  mulgcd  11693  coprmdvds1  11761  inopn  12159  basis1  12203  cnmpt2t  12451  cnmpt22  12452  cnmptcom  12456  xmeteq0  12517  sincosq1sgn  12896  sincosq2sgn  12897  sincosq3sgn  12898  sincosq4sgn  12899  speano5  13131