Theorem 3impib 1227

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

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

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 1006

This theorem is referenced by:  mob  2988  eqreu  2998  iotam  5318  funimaexglem  5413  ssimaexg  5708  funopdmsn  5834  rbropap  6409  dfsmo2  6453  3ecoptocl  6793  distrnq0  7679  addassnq0  7682  uzind  9591  fzind  9595  fnn0ind  9596  xltnegi  10070  facwordi  11003  shftvalg  11398  shftval4g  11399  mulgcd  12589  coprmdvds1  12665  pcfac  12925  mgmcl  13444  mhmlin  13552  mhmmulg  13752  issubg2m  13778  nsgbi  13793  srgmulgass  14005  dvdsrtr  14118  issubrng2  14227  issubrg2  14258  domnmuln0  14290  inopn  14730  basis1  14774  cnmpt2t  15020  cnmpt22  15021  cnmptcom  15025  xmeteq0  15086  sincosq1sgn  15553  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  speano5  16560