Theorem 3impib 1232

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

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

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 1011

This theorem is referenced by:  mob  3008  eqreu  3018  iotam  5367  funimaexglem  5462  ssimaexg  5762  funopdmsn  5889  rbropap  6508  dfsmo2  6552  3ecoptocl  6892  distrnq0  7820  addassnq0  7823  uzind  9740  fzind  9744  fnn0ind  9745  xltnegi  10220  facwordi  11161  shftvalg  11584  shftval4g  11585  mulgcd  12776  coprmdvds1  12852  pcfac  13112  mgmcl  13662  mhmlin  13757  mhmmulg  13949  issubg2m  13975  nsgbi  13990  srgmulgass  14276  dvdsrtr  14391  issubrng2  14501  issubrg2  14532  domnmuln0  14565  inopn  15087  basis1  15131  cnmpt2t  15377  cnmpt22  15378  cnmptcom  15382  xmeteq0  15443  sincosq1sgn  15910  sincosq2sgn  15911  sincosq3sgn  15912  sincosq4sgn  15913  speano5  16953