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 739  pm5.75 747  19.15 994  19.18 1046  cbv2 1159  sbied 1191  2eu6 1447  reu3 1921  sbciegft 1949  axpr 2768  fv3 3718

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