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  1725  axc9lem1  1987  axc9lem2  2026  ax12eq  2257  ax12el  2258  moanim  2336  euan  2337  eleq1a  2526  ceqsalgALT  3121  cgsexg  3128  cgsex2g  3129  cgsex4g  3130  ceqsex  3131  spc2egv  3182  spc3egv  3184  csbiebt  3440  dfiin2g  4348  ralxfrALT  4656  ordun  4969  opelxp  5019  ssrel  5081  ssrel2  5083  ssrelrel  5093  iss  5311  riotaclb  6280  iunpw  6599  limom  6700  funcnvuni  6738  fun11iun  6745  soxp  6898  tfrlem8  7055  oaordex  7209  eroveu  7408  fundmen  7591  nneneq  7702  onfin2  7711  dif1enOLD  7754  dif1en  7755  unfilem1  7786  rankwflemb  8214  sornom  8660  isf32lem9  8744  axdc3lem2  8834  axdc4lem  8838  zorn2lem3  8881  zorn2lem7  8885  tskuni  9164  grur1a  9200  grothomex  9210  genpnnp  9386  ltaddpr  9415  reclem4pr  9431  supmullem1  10516  uzin  11124  elfzmlbp  11797  sqrlem6  13063  sqreulem  13174  isprm2lem  14206  lubun  15732  lspsneq  17747  fvmptnn04ifb  19330  fbasfip  20347  alexsubALTlem2  20526  ovolunlem1  21886  dchrisum0flb  23673  brbtwn2  24186  axcontlem8  24252  usgranloopv  24356  rusgrargra  24908  frgrancvvdeqlemC  25017  grpomndo  25326  mdbr3  27194  mdbr4  27195  atssma  27275  atcvatlem  27282  ssrelf  27444  nepss  29073  fprb  29179  frrlem4  29366  nodmon  29386  nodenselem4  29420  nocvxminlem  29426  nofulllem4  29441  nofulllem5  29442  hfun  29811  supadd  30018  indexdom  30201  fdc  30214  totbndss  30249  ceqsex3OLD  30577  pm13.14  31270  isassintop  32487  tratrb  33175  ax6e2ndeq  33200  3impexpbicomVD  33525  tratrbVD  33529  equncomVD  33536  trsbcVD  33545  sbcssgVD  33551  csbingVD  33552  onfrALTVD  33559  csbsngVD  33561  csbxpgVD  33562  csbresgVD  33563  csbrngVD  33564  csbima12gALTVD  33565  csbunigVD  33566  csbfv12gALTVD  33567  con5VD  33568  hbimpgVD  33572  hbexgVD  33574  ax6e2ndeqVD  33577  bj-ax12i  34109  lsatn0  34599  lsatcmp  34603  lsatcv0  34631  lfl1dim  34721  lfl1dim2N  34722  lkrss2N  34769  lub0N  34789  glb0N  34793  ispsubcl2N  35546  cdlemefrs29bpre0  35997  dihglblem2N  36896  dihglblem3N  36897  dochsnnz  37052  rp-isfinite4  37580
  Copyright terms: Public domain W3C validator