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 581  ibib 588  pm4.71 633  bibif 678  pclem6 738  pm5.75 746  19.15 973  19.18 1026  cbv2 1146  sbied 1178  eumo0 1372  2eu6 1431  reu3 1902  reu6 1903  sbciegft 1930  fv3 3672  expeq0t 6468

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