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

Theorem biimprcd 218
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 21 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 215 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimparc  475  ax11i  1659  a9e  1956  sbie  2155  ax11eq  2277  ax11el  2278  eleq1a  2512  ceqsalg  2989  cgsexg  2996  cgsex2g  2997  cgsex4g  2998  ceqsex  2999  spc2egv  3047  spc3egv  3049  csbiebt  3289  dfiin2g  4154  ordun  4718  ralxfrALT  4777  iunpw  4794  limom  4895  opelxp  4943  ssrel  4999  ssrel2  5001  ssrelrel  5011  iss  5224  funcnvuni  5553  fun11iun  5730  soxp  6495  tfrlem8  6681  abianfp  6752  oaordex  6837  eroveu  7035  fundmen  7216  nneneq  7326  onfin2  7334  dif1enOLD  7376  dif1en  7377  unfilem1  7407  rankwflemb  7755  sornom  8195  isf32lem9  8279  axdc3lem2  8369  axdc4lem  8373  zorn2lem3  8416  zorn2lem7  8420  tskuni  8696  grur1a  8732  grothomex  8742  genpnnp  8920  ltaddpr  8949  reclem4pr  8965  supmullem1  10012  uzin  10556  sqrlem6  12091  sqreulem  12201  isprm2lem  13124  lubun  14588  lspsneq  16232  fbasfip  17938  alexsubALTlem2  18117  ovolunlem1  19431  dchrisum0flb  21242  usgranloopv  21436  grpomndo  21972  mdbr3  23838  mdbr4  23839  atssma  23919  atcvatlem  23926  nepss  25210  fprb  25432  frrlem4  25620  nodmon  25640  nodenselem4  25674  nocvxminlem  25680  nofulllem4  25695  nofulllem5  25696  brbtwn2  25879  axcontlem8  25945  hfun  26154  wl-pm5.74lem  26262  supadd  26274  indexdom  26478  fdc  26491  totbndss  26528  ceqsex3OLD  26821  pm13.14  27698  elfzmlbp  28228  rusgrargra  28543  frgrancvvdeqlemC  28600  tratrb  28792  a9e2ndeq  28818  3impexpbicomVD  29143  tratrbVD  29147  equncomVD  29154  trsbcVD  29163  sbcssVD  29169  csbingVD  29170  onfrALTVD  29177  csbsngVD  29179  csbxpgVD  29180  csbresgVD  29181  csbrngVD  29182  csbima12gALTVD  29183  csbunigVD  29184  csbfv12gALTVD  29185  con5VD  29186  hbimpgVD  29190  hbexgVD  29192  a9e2ndeqVD  29195  lubunNEW  29945  lsatn0  29971  lsatcmp  29975  lsatcv0  30003  lfl1dim  30093  lfl1dim2N  30094  lkrss2N  30141  lub0N  30161  ispsubcl2N  30918  cdlemefrs29bpre0  31367  dihglblem2N  32266  dihglblem3N  32267  dochsnnz  32422
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 179
  Copyright terms: Public domain W3C validator