Theorem pm3.27bda 423

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 418	. 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 6479  clmi1 7086  ivthlem1 7281  tgclt 7623  tgval3t 7624  cldopn 7669  cnpimaex 7762  cnima 7764  cnclima 7768  sspba 8382  sspg 8383  ssps 8385  sspn 8391  lnolin 8411  nmblore 8442  phpar 8479  ubthlem3 8527  ubthlem10 8534  ubthlem11 8535  ocorth 9159  vidfunid 10728  iddvvidd 10729  idcvvidc 10730

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