Theorem 3impib 1203

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  mob  2934  eqreu  2944  iotam  5224  funimaexglem  5315  ssimaexg  5595  rbropap  6263  dfsmo2  6307  3ecoptocl  6645  distrnq0  7483  addassnq0  7486  uzind  9389  fzind  9393  fnn0ind  9394  xltnegi  9860  facwordi  10747  shftvalg  10872  shftval4g  10873  mulgcd  12044  coprmdvds1  12118  pcfac  12377  mgmcl  12828  mhmlin  12912  mhmmulg  13096  issubg2m  13121  nsgbi  13136  srgmulgass  13336  dvdsrtr  13444  issubrng2  13550  issubrg2  13581  inopn  13940  basis1  13984  cnmpt2t  14230  cnmpt22  14231  cnmptcom  14235  xmeteq0  14296  sincosq1sgn  14684  sincosq2sgn  14685  sincosq3sgn  14686  sincosq4sgn  14687  speano5  15134