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

Theorem biimprcd 217
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 20 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 214 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  biimparc  474  ax11i  1654  a9e  1941  ax11eq  2229  ax11el  2230  eleq1a  2458  ceqsalg  2925  cgsexg  2932  cgsex2g  2933  cgsex4g  2934  ceqsex  2935  spc2egv  2983  spc3egv  2985  csbiebt  3232  dfiin2g  4068  ordun  4625  ralxfrALT  4684  iunpw  4701  limom  4802  opelxp  4850  ssrel  4906  ssrel2  4908  ssrelrel  4918  iss  5131  funcnvuni  5460  fun11iun  5637  soxp  6397  tfrlem8  6583  abianfp  6654  oaordex  6739  eroveu  6937  fundmen  7118  nneneq  7228  onfin2  7236  dif1enOLD  7278  dif1en  7279  unfilem1  7309  rankwflemb  7654  sornom  8092  isf32lem9  8176  axdc3lem2  8266  axdc4lem  8270  zorn2lem3  8313  zorn2lem7  8317  tskuni  8593  grur1a  8629  grothomex  8639  genpnnp  8817  ltaddpr  8846  reclem4pr  8862  supmullem1  9908  uzin  10452  sqrlem6  11982  sqreulem  12092  isprm2lem  13015  lubun  14479  lspsneq  16123  fbasfip  17823  alexsubALTlem2  18002  ovolunlem1  19262  dchrisum0flb  21073  usgranloop  21267  grpomndo  21784  mdbr3  23650  mdbr4  23651  atssma  23731  atcvatlem  23738  nepss  24956  fprb  25155  frrlem4  25310  nodmon  25330  nodenselem4  25364  nocvxminlem  25370  nofulllem4  25385  nofulllem5  25386  brbtwn2  25560  axcontlem8  25626  hfun  25835  wl-pm5.74lem  25943  supadd  25950  indexdom  26129  fdc  26142  totbndss  26179  ceqsex3OLD  26402  pm13.14  27280  frgrancvvdeqlemC  27793  tratrb  27965  a9e2ndeq  27991  3impexpbicomVD  28312  tratrbVD  28316  equncomVD  28323  trsbcVD  28332  sbcssVD  28338  csbingVD  28339  onfrALTVD  28346  csbsngVD  28348  csbxpgVD  28349  csbresgVD  28350  csbrngVD  28351  csbima12gALTVD  28352  csbunigVD  28353  csbfv12gALTVD  28354  con5VD  28355  hbimpgVD  28359  hbexgVD  28361  a9e2ndeqVD  28364  lubunNEW  29090  lsatn0  29116  lsatcmp  29120  lsatcv0  29148  lfl1dim  29238  lfl1dim2N  29239  lkrss2N  29286  lub0N  29306  ispsubcl2N  30063  cdlemefrs29bpre0  30512  dihglblem2N  31411  dihglblem3N  31412  dochsnnz  31567
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 178
  Copyright terms: Public domain W3C validator