MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimprcd Structured version   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  4675  ralxfrALT  4734  iunpw  4751  limom  4852  opelxp  4900  ssrel  4956  ssrel2  4958  ssrelrel  4968  iss  5181  funcnvuni  5510  fun11iun  5687  soxp  6451  tfrlem8  6637  abianfp  6708  oaordex  6793  eroveu  6991  fundmen  7172  nneneq  7282  onfin2  7290  dif1enOLD  7332  dif1en  7333  unfilem1  7363  rankwflemb  7709  sornom  8147  isf32lem9  8231  axdc3lem2  8321  axdc4lem  8325  zorn2lem3  8368  zorn2lem7  8372  tskuni  8648  grur1a  8684  grothomex  8694  genpnnp  8872  ltaddpr  8901  reclem4pr  8917  supmullem1  9964  uzin  10508  sqrlem6  12043  sqreulem  12153  isprm2lem  13076  lubun  14540  lspsneq  16184  fbasfip  17890  alexsubALTlem2  18069  ovolunlem1  19383  dchrisum0flb  21194  usgranloopv  21388  grpomndo  21924  mdbr3  23790  mdbr4  23791  atssma  23871  atcvatlem  23878  nepss  25165  fprb  25385  frrlem4  25550  nodmon  25570  nodenselem4  25604  nocvxminlem  25610  nofulllem4  25625  nofulllem5  25626  brbtwn2  25809  axcontlem8  25875  hfun  26084  wl-pm5.74lem  26192  supadd  26202  indexdom  26390  fdc  26403  totbndss  26440  ceqsex3OLD  26663  pm13.14  27541  elfzmlbp  28055  frgrancvvdeqlemC  28329  tratrb  28521  a9e2ndeq  28547  3impexpbicomVD  28870  tratrbVD  28874  equncomVD  28881  trsbcVD  28890  sbcssVD  28896  csbingVD  28897  onfrALTVD  28904  csbsngVD  28906  csbxpgVD  28907  csbresgVD  28908  csbrngVD  28909  csbima12gALTVD  28910  csbunigVD  28911  csbfv12gALTVD  28912  con5VD  28913  hbimpgVD  28917  hbexgVD  28919  a9e2ndeqVD  28922  lubunNEW  29672  lsatn0  29698  lsatcmp  29702  lsatcv0  29730  lfl1dim  29820  lfl1dim2N  29821  lkrss2N  29868  lub0N  29888  ispsubcl2N  30645  cdlemefrs29bpre0  31094  dihglblem2N  31993  dihglblem3N  31994  dochsnnz  32149
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