Theorem bi1 148

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi1

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.26im 139	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph -> ps))
5	3, 4	syl 10	1 |- ((ph <-> ps) -> (ph -> ps))

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

This theorem is referenced by:  biimp 151  biimpd 153  bii 158  pm5.74 582  ibib 589  pm4.71 634  bibif 680  pclem6 740  pm5.75 748  19.15 995  19.18 1048  cbv2 1161  sbied 1193  eumo0 1393  2eu6 1452  reu3 1927  reu6 1928  sbciegft 1955  asymref2 3432  fv3 3724  expeq0t 6525

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