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

Theorem biimprcd 216
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 19 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 213 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimparc  473  ax11i  1628  ax11eq  2132  ax11el  2133  eleq1a  2352  ceqsalg  2812  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  ceqsex  2822  spc2egv  2870  spc3egv  2872  csbiebt  3117  dfiin2g  3936  ordun  4494  ralxfrALT  4553  iunpw  4570  limom  4671  opelxp  4719  ssrel  4776  ssrelrel  4787  iss  4998  funcnvuni  5317  fun11iun  5493  soxp  6228  tfrlem8  6400  abianfp  6471  oaordex  6556  eroveu  6753  fundmen  6934  nneneq  7044  onfin2  7052  dif1enOLD  7090  dif1en  7091  unfilem1  7121  rankwflemb  7465  sornom  7903  isf32lem9  7987  axdc3lem2  8077  axdc4lem  8081  zorn2lem3  8125  zorn2lem7  8129  tskuni  8405  grur1a  8441  grothomex  8451  genpnnp  8629  ltaddpr  8658  reclem4pr  8674  supmullem1  9720  uzin  10260  sqrlem6  11733  sqreulem  11843  isprm2lem  12765  lubun  14227  lspsneq  15875  fbasfip  17563  alexsubALTlem2  17742  ovolunlem1  18856  dchrisum0flb  20659  grpomndo  21013  mdbr3  22877  mdbr4  22878  atssma  22958  atcvatlem  22965  nepss  24072  fprb  24129  frrlem4  24284  nodmon  24304  nodenselem4  24338  nocvxminlem  24344  nofulllem4  24359  nofulllem5  24360  brbtwn2  24533  axcontlem8  24599  hfun  24808  wl-pm5.74lem  24917  prl2  25169  islimrs  25580  iintlem1  25610  mrdmcd  25794  indexdom  26413  fdc  26455  totbndss  26501  ceqsex3OLD  26726  pm13.14  27609  usgranloop  28124  tratrb  28299  a9e2ndeq  28325  3impexpbicomVD  28633  tratrbVD  28637  equncomVD  28644  trsbcVD  28653  sbcssVD  28659  csbingVD  28660  onfrALTVD  28667  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  con5VD  28676  hbimpgVD  28680  hbexgVD  28682  a9e2ndeqVD  28685  lubunNEW  29163  lsatn0  29189  lsatcmp  29193  lsatcv0  29221  lfl1dim  29311  lfl1dim2N  29312  lkrss2N  29359  lub0N  29379  ispsubcl2N  30136  cdlemefrs29bpre0  30585  dihglblem2N  31484  dihglblem3N  31485  dochsnnz  31640
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 177
  Copyright terms: Public domain W3C validator