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  1657  a9e  1952  sbie  2122  ax11eq  2269  ax11el  2270  eleq1a  2504  ceqsalg  2972  cgsexg  2979  cgsex2g  2980  cgsex4g  2981  ceqsex  2982  spc2egv  3030  spc3egv  3032  csbiebt  3279  dfiin2g  4116  ordun  4674  ralxfrALT  4733  iunpw  4750  limom  4851  opelxp  4899  ssrel  4955  ssrel2  4957  ssrelrel  4967  iss  5180  funcnvuni  5509  fun11iun  5686  soxp  6450  tfrlem8  6636  abianfp  6707  oaordex  6792  eroveu  6990  fundmen  7171  nneneq  7281  onfin2  7289  dif1enOLD  7331  dif1en  7332  unfilem1  7362  rankwflemb  7708  sornom  8146  isf32lem9  8230  axdc3lem2  8320  axdc4lem  8324  zorn2lem3  8367  zorn2lem7  8371  tskuni  8647  grur1a  8683  grothomex  8693  genpnnp  8871  ltaddpr  8900  reclem4pr  8916  supmullem1  9963  uzin  10507  sqrlem6  12041  sqreulem  12151  isprm2lem  13074  lubun  14538  lspsneq  16182  fbasfip  17888  alexsubALTlem2  18067  ovolunlem1  19381  dchrisum0flb  21192  usgranloopv  21386  grpomndo  21922  mdbr3  23788  mdbr4  23789  atssma  23869  atcvatlem  23876  nepss  25163  fprb  25384  frrlem4  25539  nodmon  25559  nodenselem4  25593  nocvxminlem  25599  nofulllem4  25614  nofulllem5  25615  brbtwn2  25792  axcontlem8  25858  hfun  26067  wl-pm5.74lem  26175  supadd  26185  indexdom  26373  fdc  26386  totbndss  26423  ceqsex3OLD  26646  pm13.14  27524  elfzmlbp  28028  swrdccat3b  28106  frgrancvvdeqlemC  28286  tratrb  28475  a9e2ndeq  28501  3impexpbicomVD  28823  tratrbVD  28827  equncomVD  28834  trsbcVD  28843  sbcssVD  28849  csbingVD  28850  onfrALTVD  28857  csbsngVD  28859  csbxpgVD  28860  csbresgVD  28861  csbrngVD  28862  csbima12gALTVD  28863  csbunigVD  28864  csbfv12gALTVD  28865  con5VD  28866  hbimpgVD  28870  hbexgVD  28872  a9e2ndeqVD  28875  lubunNEW  29610  lsatn0  29636  lsatcmp  29640  lsatcv0  29668  lfl1dim  29758  lfl1dim2N  29759  lkrss2N  29806  lub0N  29826  ispsubcl2N  30583  cdlemefrs29bpre0  31032  dihglblem2N  31931  dihglblem3N  31932  dochsnnz  32087
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