Theorem bi1 164

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 163	. . 3 |- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
2		pm3.26im 153	. . 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 153	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph -> ps))
5	3, 4	syl 12	1 |- ((ph <-> ps) -> (ph -> ps))

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

This theorem is referenced by:  biimpi 167  biimpd 169  dfbi1 174  pm5.74 640  ibib 647  pm4.71 694  bibif 742  pclem6 810  pm5.75 818  pm5.75OLD 819  albi 1182  exbi 1235  cbv2 1362  sbied 1401  sbiedOLD 1402  eumo0 1628  2eu6 1695  reu6 2276  reu3 2277  sbciegft 2315  sbeqalb 2336  asymref2OLD 4122  fv3 4501  expeq0 7623  bnj925 12623  domintref 14091  inficlALT 15054  cnconn 15126  pm13.183 16055  cla4gft 16088  eqsbc3rVD 16323

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 163

Copyright terms: Public domain