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  5313  funimaexglem  5407  ssimaexg  5701  funopdmsn  5826  rbropap  6400  dfsmo2  6444  3ecoptocl  6784  distrnq0  7662  addassnq0  7665  uzind  9574  fzind  9578  fnn0ind  9579  xltnegi  10048  facwordi  10979  shftvalg  11368  shftval4g  11369  mulgcd  12558  coprmdvds1  12634  pcfac  12894  mgmcl  13413  mhmlin  13521  mhmmulg  13721  issubg2m  13747  nsgbi  13762  srgmulgass  13973  dvdsrtr  14086  issubrng2  14195  issubrg2  14226  domnmuln0  14258  inopn  14698  basis1  14742  cnmpt2t  14988  cnmpt22  14989  cnmptcom  14993  xmeteq0  15054  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  speano5  16416