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  1699  axc9lem1  1945  axc9lem2  1988  ax12eq  2242  ax12el  2243  moanim  2330  euan  2331  eleq1a  2512  ceqsalgALT  3019  cgsexg  3026  cgsex2g  3027  cgsex4g  3028  ceqsex  3029  spc2egv  3080  spc3egv  3082  csbiebt  3329  dfiin2g  4224  ralxfrALT  4532  ordun  4841  opelxp  4890  ssrel  4949  ssrel2  4951  ssrelrel  4961  iss  5175  riotaclb  6111  iunpw  6411  limom  6512  funcnvuni  6551  fun11iun  6558  soxp  6706  tfrlem8  6864  oaordex  7018  eroveu  7216  fundmen  7404  nneneq  7515  onfin2  7523  dif1enOLD  7565  dif1en  7566  unfilem1  7597  rankwflemb  8021  sornom  8467  isf32lem9  8551  axdc3lem2  8641  axdc4lem  8645  zorn2lem3  8688  zorn2lem7  8692  tskuni  8971  grur1a  9007  grothomex  9017  genpnnp  9195  ltaddpr  9224  reclem4pr  9240  supmullem1  10317  uzin  10914  elfzmlbp  11512  sqrlem6  12758  sqreulem  12868  isprm2lem  13791  lubun  15314  lspsneq  17225  fbasfip  19463  alexsubALTlem2  19642  ovolunlem1  21002  dchrisum0flb  22781  brbtwn2  23173  axcontlem8  23239  usgranloopv  23319  grpomndo  23855  mdbr3  25723  mdbr4  25724  atssma  25804  atcvatlem  25811  ssrelf  25967  nepss  27396  fprb  27606  frrlem4  27793  nodmon  27813  nodenselem4  27847  nocvxminlem  27853  nofulllem4  27868  nofulllem5  27869  hfun  28238  supadd  28444  indexdom  28654  fdc  28667  totbndss  28702  ceqsex3OLD  29031  pm13.14  29689  rusgrargra  30573  frgrancvvdeqlemC  30658  tratrb  31338  ax6e2ndeq  31364  3impexpbicomVD  31689  tratrbVD  31693  equncomVD  31700  trsbcVD  31709  sbcssgVD  31715  csbingVD  31716  onfrALTVD  31723  csbsngVD  31725  csbxpgVD  31726  csbresgVD  31727  csbrngVD  31728  csbima12gALTVD  31729  csbunigVD  31730  csbfv12gALTVD  31731  con5VD  31732  hbimpgVD  31736  hbexgVD  31738  ax6e2ndeqVD  31741  bj-ax12i  32265  lsatn0  32740  lsatcmp  32744  lsatcv0  32772  lfl1dim  32862  lfl1dim2N  32863  lkrss2N  32910  lub0N  32930  glb0N  32934  ispsubcl2N  33687  cdlemefrs29bpre0  34136  dihglblem2N  35035  dihglblem3N  35036  dochsnnz  35191
  Copyright terms: Public domain W3C validator