Theorem 3impdi 1381

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

Hypothesis

Ref	Expression
3impdi.1	|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )

Assertion

Ref	Expression
3impdi	|- ( ( ph /\ ps /\ ch ) -> th )

Proof of Theorem 3impdi

Step	Hyp	Ref	Expression
1		3impdi.1	. . 3 |- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )
2	1	anandis 873	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
3	2	3impb 1260	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  oacan  7628  omcan  7649  ecovdi  7856  distrpi  9720  axltadd  10111  ccatlcan  13472  absmulgcd  15266  axlowdimlem14  25835  fh1  28477  fh2  28478  cm2j  28479  hoadddi  28662  hosubdi  28667  leopmul2i  28994  dvconstbi  38533  eel2131  38939  uun2131  39018  uun2131p1  39019  reccot  42499  rectan  42500