Theorem 3impdi 1349

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 675	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3impb 1114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  oacan  8379  omcan  8400  ecovdi  8614  distrpi  10654  axltadd  11048  ccatlcan  14431  absmulgcd  16257  axlowdimlem14  27323  fh1  29980  fh2  29981  cm2j  29982  hoadddi  30165  hosubdi  30170  leopmul2i  30497  dvconstbi  41952  eel2131  42334  uun2131  42411  uun2131p1  42412  io1ii  46214  reccot  46460  rectan  46461