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  2946  eqreu  2956  iotam  5251  funimaexglem  5342  ssimaexg  5626  rbropap  6310  dfsmo2  6354  3ecoptocl  6692  distrnq0  7545  addassnq0  7548  uzind  9456  fzind  9460  fnn0ind  9461  xltnegi  9929  facwordi  10851  shftvalg  11020  shftval4g  11021  mulgcd  12210  coprmdvds1  12286  pcfac  12546  mgmcl  13063  mhmlin  13171  mhmmulg  13371  issubg2m  13397  nsgbi  13412  srgmulgass  13623  dvdsrtr  13735  issubrng2  13844  issubrg2  13875  domnmuln0  13907  inopn  14347  basis1  14391  cnmpt2t  14637  cnmpt22  14638  cnmptcom  14642  xmeteq0  14703  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  speano5  15698