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

Theorem biimprcd 229
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 226 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  biimparc  490  ax12i  1796  axc9lem1  2093  axc9lem2  2133  axc9lem2OLD  2134  moanim  2358  euan  2359  eleq1a  2524  ceqsalgALT  3073  cgsexg  3080  cgsex2g  3081  cgsex4g  3082  ceqsex  3083  spc2egv  3136  spc3egv  3138  csbiebt  3383  dfiin2g  4311  ralxfrALT  4619  opelxp  4864  ssrel  4923  ssrel2  4925  ssrelrel  4935  iss  5152  ordun  5524  riotaclb  6289  iunpw  6605  limom  6707  funcnvuni  6746  fun11iun  6753  soxp  6909  tfrlem8  7102  oaordex  7259  eroveu  7458  fundmen  7643  nneneq  7755  onfin2  7764  dif1en  7804  unfilem1  7835  rankwflemb  8264  sornom  8707  isf32lem9  8791  axdc3lem2  8881  axdc4lem  8885  zorn2lem3  8928  zorn2lem7  8932  tskuni  9208  grur1a  9244  grothomex  9254  genpnnp  9430  ltaddpr  9459  reclem4pr  9475  supadd  10575  supmullem1  10577  uzin  11191  elfzmlbp  11902  isfinite4  12543  brfi1uzind  12651  swrdnd  12788  sqrlem6  13311  sqreulem  13422  isprm2lem  14631  fvprmselgcd1  15003  lubun  16369  lspsneq  18345  fvmptnn04ifb  19875  fbasfip  20883  alexsubALTlem2  21063  ovolunlem1  22450  dchrisum0flb  24348  brbtwn2  24935  axcontlem8  25001  usgranloopv  25105  rusgrargra  25658  frgrancvvdeqlemC  25767  grpomndo  26074  mdbr3  27950  mdbr4  27951  atssma  28031  atcvatlem  28038  ssrelf  28221  nepss  30350  fprb  30413  frrlem4  30517  nodmon  30537  nodenselem4  30573  nocvxminlem  30579  nofulllem4  30594  nofulllem5  30595  hfun  30945  bj-ax12ig  31226  bj-ax12iOLD  31228  finxpreclem2  31782  indexdom  32061  fdc  32074  totbndss  32109  ax12eq  32512  ax12el  32513  lsatn0  32565  lsatcmp  32569  lsatcv0  32597  lfl1dim  32687  lfl1dim2N  32688  lkrss2N  32735  lub0N  32755  glb0N  32759  ispsubcl2N  33512  cdlemefrs29bpre0  33963  dihglblem2N  34862  dihglblem3N  34863  dochsnnz  35018  pm13.14  36760  tratrb  36897  ax6e2ndeq  36926  3impexpbicomVD  37253  tratrbVD  37258  equncomVD  37265  trsbcVD  37274  sbcssgVD  37280  csbingVD  37281  onfrALTVD  37288  csbsngVD  37290  csbxpgVD  37291  csbresgVD  37292  csbrngVD  37293  csbima12gALTVD  37294  csbunigVD  37295  csbfv12gALTVD  37296  con5VD  37297  hbimpgVD  37301  hbexgVD  37303  ax6e2ndeqVD  37306  isassintop  39899  zgtp1leeq  40372
  Copyright terms: Public domain W3C validator