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

Theorem biimprcd 225
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 22 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 222 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimparc  487  ax12i  1710  axc9lem1  1970  axc9lem2  2013  ax12eq  2264  ax12el  2265  moanim  2352  euan  2353  eleq1a  2550  ceqsalgALT  3139  cgsexg  3146  cgsex2g  3147  cgsex4g  3148  ceqsex  3149  spc2egv  3200  spc3egv  3202  csbiebt  3455  dfiin2g  4358  ralxfrALT  4666  ordun  4979  opelxp  5029  ssrel  5091  ssrel2  5093  ssrelrel  5103  iss  5321  riotaclb  6283  iunpw  6598  limom  6699  funcnvuni  6737  fun11iun  6744  soxp  6896  tfrlem8  7053  oaordex  7207  eroveu  7406  fundmen  7589  nneneq  7700  onfin2  7709  dif1enOLD  7752  dif1en  7753  unfilem1  7784  rankwflemb  8211  sornom  8657  isf32lem9  8741  axdc3lem2  8831  axdc4lem  8835  zorn2lem3  8878  zorn2lem7  8882  tskuni  9161  grur1a  9197  grothomex  9207  genpnnp  9383  ltaddpr  9412  reclem4pr  9428  supmullem1  10509  uzin  11114  elfzmlbp  11783  sqrlem6  13044  sqreulem  13155  isprm2lem  14083  lubun  15610  lspsneq  17568  fvmptnn04ifb  19147  fbasfip  20132  alexsubALTlem2  20311  ovolunlem1  21671  dchrisum0flb  23451  brbtwn2  23912  axcontlem8  23978  usgranloopv  24082  rusgrargra  24634  frgrancvvdeqlemC  24744  grpomndo  25052  mdbr3  26920  mdbr4  26921  atssma  27001  atcvatlem  27008  ssrelf  27167  nepss  28598  fprb  28808  frrlem4  28995  nodmon  29015  nodenselem4  29049  nocvxminlem  29055  nofulllem4  29070  nofulllem5  29071  hfun  29440  supadd  29647  indexdom  29856  fdc  29869  totbndss  29904  ceqsex3OLD  30233  pm13.14  30922  isassintop  31990  tratrb  32404  ax6e2ndeq  32430  3impexpbicomVD  32755  tratrbVD  32759  equncomVD  32766  trsbcVD  32775  sbcssgVD  32781  csbingVD  32782  onfrALTVD  32789  csbsngVD  32791  csbxpgVD  32792  csbresgVD  32793  csbrngVD  32794  csbima12gALTVD  32795  csbunigVD  32796  csbfv12gALTVD  32797  con5VD  32798  hbimpgVD  32802  hbexgVD  32804  ax6e2ndeqVD  32807  bj-ax12i  33333  lsatn0  33814  lsatcmp  33818  lsatcv0  33846  lfl1dim  33936  lfl1dim2N  33937  lkrss2N  33984  lub0N  34004  glb0N  34008  ispsubcl2N  34761  cdlemefrs29bpre0  35210  dihglblem2N  36109  dihglblem3N  36110  dochsnnz  36265
  Copyright terms: Public domain W3C validator