Theorem 3impdi 878

Description: Importation inference (undistribute conjunction).

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 512	. 2 |- ((ph /\ (ps /\ ch)) -> th)
3	2	3impb 828	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 774

This theorem is referenced by:  oacan 4172  omcan 4190  oecan 4206  ecoprdi 4311  distrpi 5006  distrpqlem 5046  axltadd 5485  expcant 6540  expordt 6541  efgh 8652  fh1t 9501  fh2t 9502  cm2jt 9503  hoadddit 9669  hosubdit 9674  leopmul2it 10006

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776

Copyright terms: Public domain