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  2998  eqreu  3008  iotam  5343  funimaexglem  5438  ssimaexg  5738  funopdmsn  5863  rbropap  6473  dfsmo2  6517  3ecoptocl  6857  distrnq0  7770  addassnq0  7773  uzind  9685  fzind  9689  fnn0ind  9690  xltnegi  10164  facwordi  11098  shftvalg  11514  shftval4g  11515  mulgcd  12705  coprmdvds1  12781  pcfac  13041  mgmcl  13561  mhmlin  13669  mhmmulg  13869  issubg2m  13895  nsgbi  13910  srgmulgass  14122  dvdsrtr  14235  issubrng2  14344  issubrg2  14375  domnmuln0  14408  inopn  14855  basis1  14899  cnmpt2t  15145  cnmpt22  15146  cnmptcom  15150  xmeteq0  15211  sincosq1sgn  15678  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  speano5  16701