Theorem 3impib 1139

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  mob  2787  eqreu  2797  funimaexglem  5053  ssimaexg  5314  dfsmo2  5987  3ecoptocl  6314  distrnq0  6939  addassnq0  6942  uzind  8767  fzind  8771  fnn0ind  8772  xltnegi  9206  facwordi  9997  shftvalg  10112  shftval4g  10113  mulgcd  10799  coprmdvds1  10867  speano5  11196