Theorem 3impib 1180

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

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

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 965

This theorem is referenced by:  mob  2870  eqreu  2880  funimaexglem  5214  ssimaexg  5491  rbropap  6148  dfsmo2  6192  3ecoptocl  6526  distrnq0  7291  addassnq0  7294  uzind  9186  fzind  9190  fnn0ind  9191  xltnegi  9648  facwordi  10518  shftvalg  10640  shftval4g  10641  mulgcd  11740  coprmdvds1  11808  inopn  12209  basis1  12253  cnmpt2t  12501  cnmpt22  12502  cnmptcom  12506  xmeteq0  12567  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  speano5  13313