Theorem 3impib 1196

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

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

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 975

This theorem is referenced by:  mob  2912  eqreu  2922  iotam  5188  funimaexglem  5279  ssimaexg  5556  rbropap  6219  dfsmo2  6263  3ecoptocl  6598  distrnq0  7408  addassnq0  7411  uzind  9310  fzind  9314  fnn0ind  9315  xltnegi  9779  facwordi  10661  shftvalg  10787  shftval4g  10788  mulgcd  11958  coprmdvds1  12032  pcfac  12289  mgmcl  12599  mhmlin  12676  inopn  12716  basis1  12760  cnmpt2t  13008  cnmpt22  13009  cnmptcom  13013  xmeteq0  13074  sincosq1sgn  13462  sincosq2sgn  13463  sincosq3sgn  13464  sincosq4sgn  13465  speano5  13901