Theorem 3impib 1225

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

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

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 1004

This theorem is referenced by:  mob  2985  eqreu  2995  iotam  5310  funimaexglem  5404  ssimaexg  5698  funopdmsn  5823  rbropap  6395  dfsmo2  6439  3ecoptocl  6779  distrnq0  7654  addassnq0  7657  uzind  9566  fzind  9570  fnn0ind  9571  xltnegi  10039  facwordi  10970  shftvalg  11355  shftval4g  11356  mulgcd  12545  coprmdvds1  12621  pcfac  12881  mgmcl  13400  mhmlin  13508  mhmmulg  13708  issubg2m  13734  nsgbi  13749  srgmulgass  13960  dvdsrtr  14073  issubrng2  14182  issubrg2  14213  domnmuln0  14245  inopn  14685  basis1  14729  cnmpt2t  14975  cnmpt22  14976  cnmptcom  14980  xmeteq0  15041  sincosq1sgn  15508  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  speano5  16331