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 679  pclem6 739  pm5.75 747  19.15 994  19.18 1046  cbv2 1159  sbied 1191  eumo0 1388  2eu6 1447  reu3 1921  reu6 1922  sbciegft 1949  asymref2 3424  asymref2OLD 3426  fv3 3718  expeq0t 6517

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