Theorem 3impib 1201

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

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

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 980

This theorem is referenced by:  mob  2919  eqreu  2929  iotam  5208  funimaexglem  5299  ssimaexg  5578  rbropap  6243  dfsmo2  6287  3ecoptocl  6623  distrnq0  7457  addassnq0  7460  uzind  9363  fzind  9367  fnn0ind  9368  xltnegi  9834  facwordi  10719  shftvalg  10844  shftval4g  10845  mulgcd  12016  coprmdvds1  12090  pcfac  12347  mgmcl  12777  mhmlin  12857  mhmmulg  13022  issubg2m  13047  nsgbi  13062  srgmulgass  13170  dvdsrtr  13268  issubrg2  13360  inopn  13473  basis1  13517  cnmpt2t  13763  cnmpt22  13764  cnmptcom  13768  xmeteq0  13829  sincosq1sgn  14217  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  speano5  14666