Theorem con2bid 344

Description: A contraposition deduction. (Contributed by NM, 15-Apr-1995.)

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 343	. 2 |- ( ( ch <-> -. ps ) <-> ( ps <-> -. ch ) )
3	1, 2	sylibr 224	1 |- ( ph -> ( ch <-> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  con1bid  345  sotric  5061  sotrieq  5062  sotr2  5064  isso2i  5067  sotri2  5525  sotri3  5526  somin1  5529  somincom  5530  ordtri2  5758  ordtr3  5769  ordintdif  5774  ord0eln0  5779  soisoi  6578  weniso  6604  ordunisuc2  7044  limsssuc  7050  nlimon  7051  tfrlem15  7488  oawordeulem  7634  nnawordex  7717  onomeneq  8150  fimaxg  8207  suplub2  8367  fiming  8404  wemapsolem  8455  cantnflem1  8586  rankval3b  8689  cardsdomel  8800  harsdom  8821  isfin1-2  9207  fin1a2lem7  9228  suplem2pr  9875  xrltnle  10105  ltnle  10117  leloe  10124  xrlttri  11972  xrleloe  11977  xrrebnd  11999  supxrbnd2  12152  supxrbnd  12158  om2uzf1oi  12752  rabssnn0fi  12785  cnpart  13980  bits0e  15151  bitsmod  15158  bitsinv1lem  15163  sadcaddlem  15179  trfil2  21691  xrsxmet  22612  metdsge  22652  ovolunlem1a  23264  ovolunlem1  23265  itg2seq  23509  toslublem  29667  tosglblem  29669  isarchi2  29739  gsumesum  30121  sgnneg  30602  sotr3  31656  noetalem3  31865  sltnle  31878  sleloe  31879  elfuns  32022  finminlem  32312  bj-bibibi  32571  itg2addnclem  33461  heiborlem10  33619  19.9alt  34252  or3or  38319  ntrclselnel2  38356  clsneifv3  38408  islininds2  42273