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

Theorem biimprcd 233
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 230 1  |-  ( ch 
->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  biimparc  495  ax12i  1804  axc9lem1  2106  axc9lem2  2146  axc9lem2OLD  2147  moanim  2378  euan  2379  eleq1a  2544  ceqsalgALT  3059  cgsexg  3066  cgsex2g  3067  cgsex4g  3068  ceqsex  3069  spc2egv  3122  spc3egv  3124  csbiebt  3369  dfiin2g  4302  ralxfrALT  4619  opelxp  4869  ssrel  4928  ssrel2  4930  ssrelrel  4940  iss  5158  ordun  5531  riotaclb  6307  iunpw  6624  limom  6726  funcnvuni  6765  fun11iun  6772  soxp  6928  tfrlem8  7120  oaordex  7277  eroveu  7476  fundmen  7661  nneneq  7773  onfin2  7782  dif1en  7822  unfilem1  7853  rankwflemb  8282  sornom  8725  isf32lem9  8809  axdc3lem2  8899  axdc4lem  8903  zorn2lem3  8946  zorn2lem7  8950  tskuni  9226  grur1a  9262  grothomex  9272  genpnnp  9448  ltaddpr  9477  reclem4pr  9493  supadd  10597  supmullem1  10599  uzin  11215  elfzmlbp  11927  isfinite4  12581  brfi1uzind  12692  brfi1uzindOLD  12698  swrdnd  12842  sqrlem6  13388  sqreulem  13499  isprm2lem  14710  fvprmselgcd1  15082  lubun  16447  lspsneq  18423  fvmptnn04ifb  19952  fbasfip  20961  alexsubALTlem2  21141  ovolunlem1  22528  dchrisum0flb  24427  brbtwn2  25014  axcontlem8  25080  usgranloopv  25184  rusgrargra  25737  frgrancvvdeqlemC  25846  grpomndo  26155  mdbr3  28031  mdbr4  28032  atssma  28112  atcvatlem  28119  ssrelf  28297  nepss  30422  fprb  30484  frrlem4  30588  nodmon  30608  nodenselem4  30644  nocvxminlem  30650  nofulllem4  30665  nofulllem5  30666  hfun  31016  bj-ax12ig  31290  bj-ax12iOLD  31292  finxpreclem2  31852  indexdom  32125  fdc  32138  totbndss  32173  ax12eq  32576  ax12el  32577  lsatn0  32636  lsatcmp  32640  lsatcv0  32668  lfl1dim  32758  lfl1dim2N  32759  lkrss2N  32806  lub0N  32826  glb0N  32830  ispsubcl2N  33583  cdlemefrs29bpre0  34034  dihglblem2N  34933  dihglblem3N  34934  dochsnnz  35089  pm13.14  36830  tratrb  36967  ax6e2ndeq  36996  3impexpbicomVD  37316  tratrbVD  37321  equncomVD  37328  trsbcVD  37337  sbcssgVD  37343  csbingVD  37344  onfrALTVD  37351  csbsngVD  37353  csbxpgVD  37354  csbresgVD  37355  csbrngVD  37356  csbima12gALTVD  37357  csbunigVD  37358  csbfv12gALTVD  37359  con5VD  37360  hbimpgVD  37364  hbexgVD  37366  ax6e2ndeqVD  37369  isassintop  40354  zgtp1leeq  40827
  Copyright terms: Public domain W3C validator