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

Theorem biimprcd 228
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 23 . 2  |-  ( ch 
->  ch )
2 biimpcd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibrcom 225 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  biimparc  489  ax12i  1785  axc9lem1  2054  axc9lem2  2093  moanim  2323  euan  2324  eleq1a  2503  ceqsalgALT  3104  cgsexg  3111  cgsex2g  3112  cgsex4g  3113  ceqsex  3114  spc2egv  3165  spc3egv  3167  csbiebt  3412  dfiin2g  4326  ralxfrALT  4632  opelxp  4875  ssrel  4934  ssrel2  4936  ssrelrel  4946  iss  5163  ordun  5534  riotaclb  6295  iunpw  6610  limom  6712  funcnvuni  6751  fun11iun  6758  soxp  6911  tfrlem8  7101  oaordex  7258  eroveu  7457  fundmen  7641  nneneq  7752  onfin2  7761  dif1en  7801  unfilem1  7832  rankwflemb  8254  sornom  8696  isf32lem9  8780  axdc3lem2  8870  axdc4lem  8874  zorn2lem3  8917  zorn2lem7  8921  tskuni  9197  grur1a  9233  grothomex  9243  genpnnp  9419  ltaddpr  9448  reclem4pr  9464  supadd  10564  supmullem1  10566  uzin  11180  elfzmlbp  11889  isfinite4  12529  swrdnd  12762  sqrlem6  13279  sqreulem  13390  isprm2lem  14591  fvprmselgcd1  14955  lubun  16313  lspsneq  18273  fvmptnn04ifb  19799  fbasfip  20807  alexsubALTlem2  20987  ovolunlem1  22324  dchrisum0flb  24208  brbtwn2  24778  axcontlem8  24844  usgranloopv  24948  rusgrargra  25500  frgrancvvdeqlemC  25609  grpomndo  25916  mdbr3  27782  mdbr4  27783  atssma  27863  atcvatlem  27870  ssrelf  28057  nepss  30135  fprb  30197  frrlem4  30301  nodmon  30321  nodenselem4  30355  nocvxminlem  30361  nofulllem4  30376  nofulllem5  30377  hfun  30727  bj-ax12i  31002  indexdom  31765  fdc  31778  totbndss  31813  ceqsex3OLD  32140  ax12eq  32221  ax12el  32222  lsatn0  32274  lsatcmp  32278  lsatcv0  32306  lfl1dim  32396  lfl1dim2N  32397  lkrss2N  32444  lub0N  32464  glb0N  32468  ispsubcl2N  33221  cdlemefrs29bpre0  33672  dihglblem2N  34571  dihglblem3N  34572  dochsnnz  34727  pm13.14  36401  tratrb  36538  ax6e2ndeq  36567  3impexpbicomVD  36897  tratrbVD  36902  equncomVD  36909  trsbcVD  36918  sbcssgVD  36924  csbingVD  36925  onfrALTVD  36932  csbsngVD  36934  csbxpgVD  36935  csbresgVD  36936  csbrngVD  36937  csbima12gALTVD  36938  csbunigVD  36939  csbfv12gALTVD  36940  con5VD  36941  hbimpgVD  36945  hbexgVD  36947  ax6e2ndeqVD  36950  isassintop  38617  zgtp1leeq  39093
  Copyright terms: Public domain W3C validator