Theorem bi2 165

Description: Property of the biconditional connective.

Assertion

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

Proof of Theorem bi2

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.27im 154	. 2 |- (-. ((ph -> ps) -> -. (ps -> ph)) -> (ps -> ph))
5	3, 4	syl 12	1 |- ((ph <-> ps) -> (ps -> ph))

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

This theorem is referenced by:  biimpri 168  biimprd 170  dfbi1 174  exbiri 419  pm5.74 640  pm4.72 700  pclem6 810  pm5.75 818  pm5.75OLD 819  exbir 1127  albi 1182  exbi 1235  cbv2 1362  sbied 1401  sbiedOLD 1402  2eu6 1695  euind 2272  reu6 2276  reuind 2283  sbciegft 2315  sbsslem 2802  axpr 3338  fv3 4501  iota4 4911  bnj1126 12724  ax10ext 16046  pm13.192 16056  euunianOLD 16078  trsspwALT 16299  trsspwALT2 16300  sspwtr 16302  sspwtrALT 16303  pwtrVD 16305  pwtrrVD 16307  snssiALTVD 16309  sstrALT2VD 16317  sstrALT2 16318  suctrALT2VD 16319  eqsbc3rVD 16323  pm3.26bi2VD 16329  exbirVD 16336  exbiriVD 16337

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