Theorem con2bid 528

Description: A contraposition deduction.

Hypothesis

Ref	Expression
con2bid.1	|- (ph -> (ps <-> -. ch))

Assertion

Ref	Expression
con2bid	|- (ph -> (ch <-> -. ps))

Proof of Theorem con2bid

Step	Hyp	Ref	Expression
1		con2bid.1	. 2 |- (ph -> (ps <-> -. ch))
2		con2bi 527	. 2 |- ((ch <-> -. ps) <-> (ps <-> -. ch))
3	1, 2	sylibr 200	1 |- (ph -> (ch <-> -. ps))

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

This theorem is referenced by:  con1bid 529  necon2abid 1625  necon2bbid 1626  r19.9rzv 2353  sotric 2866  sotrieq 2867  so 2870  ordtri2 2988  ord0eln0 3029  ordunisuc2 3121  limsssuc 3127  nlimon 3128  oawordeulem 4194  onomeneq 4525  rankr1 4684  ondomcard 4868  prlem934b 5150  suplem2pr 5174  sqgt0sr 5227  suppsr2 5235  suppsr3 5236  xrltnlet 5514  ltnlet 5523  leloet 5530  xrlttrit 5564  xrleloet 5569  xrrebndt 5580  supxrbnd 6093  supxrbnd2 6098  elnnz1 6157  om2uzf1o 6302

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  df-an 225

Copyright terms: Public domain