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  2987  eqreu  2997  iotam  5320  funimaexglem  5415  ssimaexg  5711  funopdmsn  5837  rbropap  6414  dfsmo2  6458  3ecoptocl  6798  distrnq0  7684  addassnq0  7687  uzind  9596  fzind  9600  fnn0ind  9601  xltnegi  10075  facwordi  11008  shftvalg  11419  shftval4g  11420  mulgcd  12610  coprmdvds1  12686  pcfac  12946  mgmcl  13465  mhmlin  13573  mhmmulg  13773  issubg2m  13799  nsgbi  13814  srgmulgass  14026  dvdsrtr  14139  issubrng2  14248  issubrg2  14279  domnmuln0  14311  inopn  14756  basis1  14800  cnmpt2t  15046  cnmpt22  15047  cnmptcom  15051  xmeteq0  15112  sincosq1sgn  15579  sincosq2sgn  15580  sincosq3sgn  15581  sincosq4sgn  15582  speano5  16599