Theorem 3impdi 1351

Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)

Hypothesis

Ref	Expression
3impdi.1	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3impdi	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impdi

Step	Hyp	Ref	Expression
1		3impdi.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃)
2	1	anandis 678	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3impb 1114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  oacan  8489  omcan  8510  ecovdi  8775  distrpi  10827  axltadd  11223  ccatlcan  14659  absmulgcd  16495  axlowdimlem14  28858  fh1  31520  fh2  31521  cm2j  31522  hoadddi  31705  hosubdi  31710  leopmul2i  32037  dvconstbi  44296  eel2131  44676  uun2131  44753  uun2131p1  44754  io1ii  48882  reccot  49720  rectan  49721