Theorem 3impib 1206

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

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

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 985

This theorem is referenced by:  mob  2965  eqreu  2975  iotam  5286  funimaexglem  5380  ssimaexg  5669  funopdmsn  5792  rbropap  6359  dfsmo2  6403  3ecoptocl  6741  distrnq0  7614  addassnq0  7617  uzind  9526  fzind  9530  fnn0ind  9531  xltnegi  9999  facwordi  10929  shftvalg  11313  shftval4g  11314  mulgcd  12503  coprmdvds1  12579  pcfac  12839  mgmcl  13358  mhmlin  13466  mhmmulg  13666  issubg2m  13692  nsgbi  13707  srgmulgass  13918  dvdsrtr  14030  issubrng2  14139  issubrg2  14170  domnmuln0  14202  inopn  14642  basis1  14686  cnmpt2t  14932  cnmpt22  14933  cnmptcom  14937  xmeteq0  14998  sincosq1sgn  15465  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  speano5  16217