Theorem 3impib 1144

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 255	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1140	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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

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

This theorem is referenced by:  mob  2811  eqreu  2821  funimaexglem  5131  ssimaexg  5401  dfsmo2  6090  3ecoptocl  6421  distrnq0  7115  addassnq0  7118  uzind  8956  fzind  8960  fnn0ind  8961  xltnegi  9401  facwordi  10279  shftvalg  10401  shftval4g  10402  mulgcd  11448  coprmdvds1  11516  inopn  11870  basis1  11913  xmeteq0  12161  speano5  12563