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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mob  3008  eqreu  3018  iotam  5369  funimaexglem  5464  ssimaexg  5765  funopdmsn  5895  rbropap  6514  dfsmo2  6558  3ecoptocl  6898  distrnq0  7826  addassnq0  7829  uzind  9759  fzind  9763  fnn0ind  9764  xltnegi  10239  facwordi  11180  shftvalg  11603  shftval4g  11604  mulgcd  12795  coprmdvds1  12871  pcfac  13131  mgmcl  13681  mhmlin  13776  mhmmulg  13968  issubg2m  13994  nsgbi  14009  srgmulgass  14295  dvdsrtr  14410  issubrng2  14520  issubrg2  14551  domnmuln0  14584  inopn  15106  basis1  15150  cnmpt2t  15396  cnmpt22  15397  cnmptcom  15401  xmeteq0  15462  sincosq1sgn  15930  sincosq2sgn  15931  sincosq3sgn  15932  sincosq4sgn  15933  speano5  16982