Theorem 3impdi 880

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 829	1 |- ((ph /\ ps /\ ch) -> th)

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

This theorem is referenced by:  oacan 4182  omcan 4200  oecan 4216  ecoprdi 4321  distrpi 5026  distrpqlem 5066  axltadd 5505  expcant 6601  expordt 6602  efgh 8718  fh1t 9561  fh2t 9562  cm2jt 9563  hoadddit 9729  hosubdit 9734  leopmul2it 10068

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 777

Copyright terms: Public domain