Theorem 3impdi 1152

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

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  oacan 5229  omcan 5248  oecan 5264  ecoprdi 5380  distrpi 6178  distrpqlem 6218  axltadd 6674  expcan 7846  expord 7847  efgh 10072  fh1 11194  fh2 11195  cm2j 11196  hoadddi 11366  hosubdi 11371  leopmul2i 11706  mulgcd 13763  absmulgcd 13764  dvdsgcd 13765

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 164  df-an 242  df-3an 860

Copyright terms: Public domain