Theorem con2bid 525

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 524	. 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 526  necon2abid 1619  necon2bbid 1620  r19.9rzv 2345  sotric 2855  sotrieq 2856  so 2859  ordtri2 2977  ord0eln0 3018  ordunisuc2 3110  limsssuc 3116  nlimon 3117  oawordeulem 4178  onomeneq 4504  rankr1 4654  ondomcard 4837  prlem934b 5118  suplem2pr 5142  sqgt0sr 5195  suppsr2 5203  suppsr3 5204  xrltnlet 5482  ltnlet 5491  leloet 5499  xrlttrit 5533  xrleloet 5538  xrrebndt 5549  supxrbnd 6046  supxrbnd2 6051  elnnz1 6110  om2uzf1o 6246

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