Theorem 3impdi 892

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

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  oacan 4240  omcan 4258  oecan 4274  ecoprdi 4382  distrpi 5091  distrpqlem 5131  axltadd 5570  expcan 6690  expord 6691  efgh 8801  fh1 9644  fh2 9645  cm2j 9646  hoadddi 9812  hosubdi 9817  leopmul2i 10151

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 154  df-an 232  df-3an 789

Copyright terms: Public domain