Theorem 3impib 1228

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

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

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 1007

This theorem is referenced by:  mob  3001  eqreu  3011  iotam  5346  funimaexglem  5441  ssimaexg  5741  funopdmsn  5866  rbropap  6476  dfsmo2  6520  3ecoptocl  6860  distrnq0  7779  addassnq0  7782  uzind  9695  fzind  9699  fnn0ind  9700  xltnegi  10174  facwordi  11110  shftvalg  11529  shftval4g  11530  mulgcd  12720  coprmdvds1  12796  pcfac  13056  mgmcl  13593  mhmlin  13701  mhmmulg  13901  issubg2m  13927  nsgbi  13942  srgmulgass  14154  dvdsrtr  14268  issubrng2  14378  issubrg2  14409  domnmuln0  14442  inopn  14917  basis1  14961  cnmpt2t  15207  cnmpt22  15208  cnmptcom  15212  xmeteq0  15273  sincosq1sgn  15740  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  speano5  16763