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  2228  ax11el  2229  eleq1a  2457  ceqsalg  2924  cgsexg  2931  cgsex2g  2932  cgsex4g  2933  ceqsex  2934  spc2egv  2982  spc3egv  2984  csbiebt  3231  dfiin2g  4067  ordun  4624  ralxfrALT  4683  iunpw  4700  limom  4801  opelxp  4849  ssrel  4905  ssrel2  4907  ssrelrel  4917  iss  5130  funcnvuni  5459  fun11iun  5636  soxp  6396  tfrlem8  6582  abianfp  6653  oaordex  6738  eroveu  6936  fundmen  7117  nneneq  7227  onfin2  7235  dif1enOLD  7277  dif1en  7278  unfilem1  7308  rankwflemb  7653  sornom  8091  isf32lem9  8175  axdc3lem2  8265  axdc4lem  8269  zorn2lem3  8312  zorn2lem7  8316  tskuni  8592  grur1a  8628  grothomex  8638  genpnnp  8816  ltaddpr  8845  reclem4pr  8861  supmullem1  9907  uzin  10451  sqrlem6  11981  sqreulem  12091  isprm2lem  13014  lubun  14478  lspsneq  16122  fbasfip  17822  alexsubALTlem2  18001  ovolunlem1  19261  dchrisum0flb  21072  usgranloop  21266  grpomndo  21783  mdbr3  23649  mdbr4  23650  atssma  23730  atcvatlem  23737  nepss  24955  fprb  25154  frrlem4  25309  nodmon  25329  nodenselem4  25363  nocvxminlem  25369  nofulllem4  25384  nofulllem5  25385  brbtwn2  25559  axcontlem8  25625  hfun  25834  wl-pm5.74lem  25942  supadd  25949  indexdom  26128  fdc  26141  totbndss  26178  ceqsex3OLD  26401  pm13.14  27279  frgrancvvdeqlemC  27792  tratrb  27964  a9e2ndeq  27990  3impexpbicomVD  28311  tratrbVD  28315  equncomVD  28322  trsbcVD  28331  sbcssVD  28337  csbingVD  28338  onfrALTVD  28345  csbsngVD  28347  csbxpgVD  28348  csbresgVD  28349  csbrngVD  28350  csbima12gALTVD  28351  csbunigVD  28352  csbfv12gALTVD  28353  con5VD  28354  hbimpgVD  28358  hbexgVD  28360  a9e2ndeqVD  28363  lubunNEW  29089  lsatn0  29115  lsatcmp  29119  lsatcv0  29147  lfl1dim  29237  lfl1dim2N  29238  lkrss2N  29285  lub0N  29305  ispsubcl2N  30062  cdlemefrs29bpre0  30511  dihglblem2N  31410  dihglblem3N  31411  dochsnnz  31566
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