Theorem 3impib 1203

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

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

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 982

This theorem is referenced by:  mob  2946  eqreu  2956  iotam  5251  funimaexglem  5342  ssimaexg  5624  rbropap  6303  dfsmo2  6347  3ecoptocl  6685  distrnq0  7529  addassnq0  7532  uzind  9440  fzind  9444  fnn0ind  9445  xltnegi  9913  facwordi  10835  shftvalg  11004  shftval4g  11005  mulgcd  12194  coprmdvds1  12270  pcfac  12530  mgmcl  13028  mhmlin  13125  mhmmulg  13319  issubg2m  13345  nsgbi  13360  srgmulgass  13571  dvdsrtr  13683  issubrng2  13792  issubrg2  13823  domnmuln0  13855  inopn  14265  basis1  14309  cnmpt2t  14555  cnmpt22  14556  cnmptcom  14560  xmeteq0  14621  sincosq1sgn  15088  sincosq2sgn  15089  sincosq3sgn  15090  sincosq4sgn  15091  speano5  15616