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  8512  omcan  8533  ecovdi  8798  distrpi  10851  axltadd  11247  ccatlcan  14683  absmulgcd  16519  axlowdimlem14  28882  fh1  31547  fh2  31548  cm2j  31549  hoadddi  31732  hosubdi  31737  leopmul2i  32064  dvconstbi  44323  eel2131  44703  uun2131  44780  uun2131p1  44781  io1ii  48909  reccot  49747  rectan  49748