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  dfbi1 158  pm5.74 583  ibib 590  pm4.71 635  bibif 681  pclem6 741  pm5.75 749  19.15 997  19.18 1050  cbv2 1163  sbied 1195  eumo0 1395  2eu6 1454  reu3 1929  reu6 1930  sbciegft 1957  asymref2 3438  fv3 3731  expeq0t 6545

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