Theorem bi2 149

Description: Property of the biconditional connective.

Assertion

Ref	Expression
bi2	|- ((ph <-> ps) -> (ps -> ph))

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		df-bi 147	. . 3 |- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
2		pm3.26im 139	. . 3 |- (-. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps))) -> ((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))))
3	1, 2	ax-mp 7	. 2 |- ((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph)))
4		pm3.27im 140	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ps -> ph))
5	3, 4	syl 10	1 |- ((ph <-> ps) -> (ps -> ph))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  biimpr 152  biimprd 154  bii 158  pm5.74 581  pm4.72 639  pclem6 738  pm5.75 746  19.15 973  19.18 1026  cbv2 1146  sbied 1178  2eu6 1431  reu3 1902  sbciegft 1930  axpr 2746  fv3 3672

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

Copyright terms: Public domain