Theorem 3impdi 1346

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oacan  8173  omcan  8194  ecovdi  8404  distrpi  10319  axltadd  10713  ccatlcan  14079  absmulgcd  15896  axlowdimlem14  26740  fh1  29394  fh2  29395  cm2j  29396  hoadddi  29579  hosubdi  29584  leopmul2i  29911  dvconstbi  40664  eel2131  41046  uun2131  41123  uun2131p1  41124  reccot  44856  rectan  44857