MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprcd Unicode version

Theorem biimprcd 216
Description: Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
Hypothesis
Ref Expression
biimpcd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprcd  |-  ( ch 
->  ( ph  ->  ps ) )

Proof of Theorem biimprcd
StepHypRef Expression
1 id 19 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 213 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimparc  473  ax11i  1637  ax11eq  2145  ax11el  2146  eleq1a  2365  ceqsalg  2825  cgsexg  2832  cgsex2g  2833  cgsex4g  2834  ceqsex  2835  spc2egv  2883  spc3egv  2885  csbiebt  3130  dfiin2g  3952  ordun  4510  ralxfrALT  4569  iunpw  4586  limom  4687  opelxp  4735  ssrel  4792  ssrelrel  4803  iss  5014  funcnvuni  5333  fun11iun  5509  soxp  6244  tfrlem8  6416  abianfp  6487  oaordex  6572  eroveu  6769  fundmen  6950  nneneq  7060  onfin2  7068  dif1enOLD  7106  dif1en  7107  unfilem1  7137  rankwflemb  7481  sornom  7919  isf32lem9  8003  axdc3lem2  8093  axdc4lem  8097  zorn2lem3  8141  zorn2lem7  8145  tskuni  8421  grur1a  8457  grothomex  8467  genpnnp  8645  ltaddpr  8674  reclem4pr  8690  supmullem1  9736  uzin  10276  sqrlem6  11749  sqreulem  11859  isprm2lem  12781  lubun  14243  lspsneq  15891  fbasfip  17579  alexsubALTlem2  17758  ovolunlem1  18872  dchrisum0flb  20675  grpomndo  21029  mdbr3  22893  mdbr4  22894  atssma  22974  atcvatlem  22981  nepss  24087  fprb  24200  frrlem4  24355  nodmon  24375  nodenselem4  24409  nocvxminlem  24415  nofulllem4  24430  nofulllem5  24431  brbtwn2  24605  axcontlem8  24671  hfun  24880  wl-pm5.74lem  24989  supadd  24996  prl2  25272  islimrs  25683  iintlem1  25713  mrdmcd  25897  indexdom  26516  fdc  26558  totbndss  26604  ceqsex3OLD  26829  pm13.14  27712  usgranloop  28258  tratrb  28598  a9e2ndeq  28624  3impexpbicomVD  28949  tratrbVD  28953  equncomVD  28960  trsbcVD  28969  sbcssVD  28975  csbingVD  28976  onfrALTVD  28983  csbsngVD  28985  csbxpgVD  28986  csbresgVD  28987  csbrngVD  28988  csbima12gALTVD  28989  csbunigVD  28990  csbfv12gALTVD  28991  con5VD  28992  hbimpgVD  28996  hbexgVD  28998  a9e2ndeqVD  29001  lubunNEW  29785  lsatn0  29811  lsatcmp  29815  lsatcv0  29843  lfl1dim  29933  lfl1dim2N  29934  lkrss2N  29981  lub0N  30001  ispsubcl2N  30758  cdlemefrs29bpre0  31207  dihglblem2N  32106  dihglblem3N  32107  dochsnnz  32262
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator