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  3002  eqreu  3012  iotam  5349  funimaexglem  5444  ssimaexg  5744  funopdmsn  5869  rbropap  6487  dfsmo2  6531  3ecoptocl  6871  distrnq0  7790  addassnq0  7793  uzind  9710  fzind  9714  fnn0ind  9715  xltnegi  10190  facwordi  11130  shftvalg  11549  shftval4g  11550  mulgcd  12740  coprmdvds1  12816  pcfac  13076  mgmcl  13625  mhmlin  13725  mhmmulg  13919  issubg2m  13945  nsgbi  13960  srgmulgass  14235  dvdsrtr  14349  issubrng2  14459  issubrg2  14490  domnmuln0  14523  inopn  14997  basis1  15041  cnmpt2t  15287  cnmpt22  15288  cnmptcom  15292  xmeteq0  15353  sincosq1sgn  15820  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  speano5  16853