Theorem pm3.27bda 421

Description: Deduction eliminating a conjunct.

Hypothesis

Ref	Expression
pm3.26bda.1	|- (ph -> (ps <-> (ch /\ th)))

Assertion

Ref	Expression
pm3.27bda	|- ((ph /\ ps) -> th)

Proof of Theorem pm3.27bda

Step	Hyp	Ref	Expression
1		pm3.26bda.1	. . 3 |- (ph -> (ps <-> (ch /\ th)))
2	1	biimpa 416	. 2 |- ((ph /\ ps) -> (ch /\ th))
3	2	pm3.27d 325	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  elfzuz3t 6478  clmi1 7086  ivthlem1 7281  tgclt 7624  tgval3t 7625  cldopn 7672  cnpimaex 7765  cnima 7767  cnclima 7771  sspba 8386  sspg 8387  ssps 8389  sspn 8395  lnolin 8415  nmblore 8446  phpar 8483  ubthlem3 8531  ubthlem10 8538  ubthlem11 8539  ocorth 9164  vidfunid 10757  iddvvidd 10758  idcvvidc 10759

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

Copyright terms: Public domain