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

Theorem biimprd 227
Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 202 and biimpri 210. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimprd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimprd  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem biimprd
StepHypRef Expression
1 id 22 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 225 1  |-  ( ph  ->  ( ch  ->  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:  syl6bir  233  mpbird  236  sylibrd  238  sylbird  239  con4bid  295  mtbid  302  mtbii  304  imbi1d  319  biimpar  488  prlem1  973  alexbii  1705  spfw  1875  cbvalw  1877  alcomiw  1880  ax12v  1934  nfimd  2000  axc11nlem  2021  cbvalv1  2064  cbval  2114  axc11nlemALT  2142  axc16i  2156  equvini  2179  axc16gALT  2196  sbequi  2204  eqrdav  2450  pm13.18  2705  rspcimdv  3151  rspcedv  3154  moi2  3219  moi  3221  eqrd  3450  sspsstr  3538  eqoreldif  4013  ralxfrd  4614  ralxfr2d  4616  isso2i  4787  wefrc  4828  elres  5140  sotri3  5230  oneqmini  5474  ordsssuc2  5511  ordtri2or  5518  2elresin  5687  f1ocnv  5826  tz6.12c  5884  fveqres  5899  fvun1  5936  dffo4  6038  fconst5  6122  fnprb  6123  isores3  6226  f1owe  6244  weniso  6245  ndmovordi  6460  orduniorsuc  6657  ordzsl  6672  tfinds  6686  f1oweALT  6777  fnse  6913  tposfo2  6996  wfrlem5  7040  wfrlem12  7047  issmo2  7068  iordsmo  7076  smoel2  7082  tz7.48lem  7158  oawordeulem  7255  om00  7276  omlimcl  7279  odi  7280  nnawordi  7322  fiint  7848  fipreima  7880  dffi2  7937  suplub2  7975  wemapsolem  8065  unwdomg  8099  inf3lem3  8135  trcl  8212  fidomtri  8427  prdom2  8437  cardaleph  8520  ackbij1lem16  8665  coflim  8691  coftr  8703  infpssrlem4  8736  isfin7-2  8826  axdc3lem2  8881  axdc3lem4  8883  brdom6disj  8960  entric  8982  fpwwe2lem12  9066  inatsk  9203  grur1a  9244  indpi  9332  reclem3pr  9474  supsrlem  9535  lelttr  9724  dedekindle  9798  negn0  10048  fimaxre  10551  nnmulcl  10632  arch  10866  nnnegz  10940  zeo  11021  uzm1  11189  rpneg  11332  xrlttri  11438  xrlelttr  11453  iccid  11681  icoshft  11754  fzen  11816  elfz2nn0  11885  elfzom1p1elfzo  11993  fleqceilz  12081  zmodidfzoimp  12127  hasheqf1oi  12534  hashnfinnn0  12542  swrd0  12790  swrdccatin12lem2  12845  swrdccat  12849  swrdccat3blem  12851  repswswrd  12887  trclublem  13059  max0add  13373  abslt  13377  absle  13378  rexuzre  13415  caurcvg  13742  caurcvgOLD  13743  caucvg  13745  dvdsval2  14308  negdvdsb  14319  muldvds2  14328  smuval2  14456  smupvallem  14457  rplpwr  14524  alginv  14534  algfx  14539  prmgt1  14643  coprmgcdb  14654  rpexp1i  14673  qnumdencl  14688  phiprmpw  14724  prmdiveq  14734  pcmpt  14837  infpnlem1  14854  prmgaplem3  15023  prmgaplem8  15028  imasaddfnlem  15434  plelttr  16218  lubval  16230  lublecllem  16234  glbval  16243  mrcmndind  16613  mndodconglem  17190  elfrlmbasn0  19325  mavmulsolcl  19576  slesolex  19707  fvmptnn04if  19873  chfacfisf  19878  chfacfisfcpmat  19879  cnpnei  20280  uncon  20444  comppfsc  20547  kqsat  20746  isr0  20752  qtophmeo  20832  trufil  20925  alexsubALT  21066  cnextcn  21082  ucnima  21296  iducn  21298  bl2in  21415  addcnlem  21896  rescncf  21929  ovoliunlem2  22456  voliun  22507  mbflimsup  22623  mbflimsupOLD  22624  itgcn  22800  dvdsq1p  23111  aalioulem2  23289  recosf1o  23484  logrec  23700  xrlimcnp  23894  basellem4  24010  bposlem1  24212  bposlem5  24216  lgsdchrval  24275  pntlem3  24447  brbtwn2  24935  axbtwnid  24969  usgraedgprv  25103  usgraedgrnv  25104  usgrafisinds  25141  iswlkg  25252  wwlkextinj  25458  isclwlkg  25483  clwlkisclwwlklem2a1  25507  clwwisshclww  25535  clwlksizeeq  25580  eupai  25695  numclwwlkovf2ex  25814  numclwwlk2lem1  25830  numclwwlk5lem  25839  frgrareggt1  25844  friendship  25850  elghomlem2OLD  26090  blocn2  26449  htthlem  26570  axhcompl-zf  26651  spanuni  27197  spansncol  27221  spansneleq  27223  elspansn5  27227  idcnop  27634  pjnormssi  27821  dmdmd  27953  bian1d  28100  ifeqeqx  28158  supxrnemnf  28354  rexdiv  28395  xrstos  28441  xrge0omnd  28474  cnre2csqlem  28716  fsumcvg4  28756  lmxrge0  28758  qqhval2lem  28785  esumpr2  28888  esumcvg  28907  issgon  28945  measxun2  29032  measres  29044  measdivcstOLD  29046  measdivcst  29047  elorrvc  29296  signsply0  29440  bnj580  29724  erdsze2lem2  29927  cvmsval  29989  ghomgsg  30311  ghomf1olem  30312  fundmpss  30407  dfon2lem3  30431  frmin  30480  poseq  30491  soseq  30492  frrlem5  30518  frrlem11  30526  nobndup  30589  nobnddown  30590  dfrdg4  30718  cgrtriv  30769  btwntriv2  30779  ifscgr  30811  lineext  30843  btwnconn1lem12  30865  colinbtwnle  30885  elicc3  30973  ontgval  31091  onsucconi  31097  bj-bibibi  31170  bj-cbvexw  31273  bj-axc11nlemv  31347  bj-equsal  31428  bj-elid  31640  bj-finsumval0  31702  relowlssretop  31766  sucneqond  31768  finxpsuc  31790  wl-nfs1t  31871  wl-ax12v2  31909  finixpnum  31930  ltflcei  31933  poimirlem23  31963  poimirlem24  31964  poimirlem27  31967  poimirlem32  31972  itg2addnclem  31993  areacirclem2  32033  areacirclem5  32036  areacirc  32037  nninfnub  32080  prdstotbnd  32126  heiborlem4  32146  heibor  32153  grpokerinj  32183  isidlc  32248  prtlem17  32448  dral1-o  32474  axc16g-o  32505  lsator0sp  32567  atlrelat1  32887  cvratlem  32986  diaintclN  34626  dibintclN  34735  cdlemn11pre  34778  dihord2pre  34793  dihintcl  34912  dochkrshp4  34957  lcfrlem9  35118  lcfrlem21  35131  mapdh8e  35352  elrfirn2  35538  rencldnfilem  35663  sdrgacs  36067  refimssco  36213  rtrclex  36224  intimasn  36249  ss2iundf  36251  ov2ssiunov2  36292  comptiunov2i  36298  iunrelexpuztr  36311  snelpwrVD  37227  en3lplem1VD  37239  en3lpVD  37241  orbi1rVD  37244  sbc3orgVD  37247  3impexpVD  37252  equncomVD  37265  trsbcVD  37274  trintALTVD  37277  trintALT  37278  csbingVD  37281  csbsngVD  37290  csbxpgVD  37291  csbrngVD  37293  csbfv12gALTVD  37296  relopabVD  37298  e2ebindVD  37309  stoweidlem35  37896  stoweidlem48  37909  rexrsb  38590  funbrafv  38660  rlimdmafv  38679  fzopredsuc  38720  iccpartlt  38738  nnsum3primesle9  38889  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  pfxccatin12lem2  38965  funopsn  39018  fzoopth  39063  2ffzoeq  39064  umgredgprv  39195  umgrpredgav  39230  usgredgprvALT  39278  fusgrfisstep  39395  fusgrfis  39396  nbupgr  39412  nbumgrvtx  39414  usgedgvadf1lem2  39779  usgedgvadf1ALTlem2  39782  usgfis  39811  usgfisALT  39815  usgrafiedgALT  39816  mgm2mgm  39916  2zrngnmlid  40002  2zrngnmrid  40003  ellcoellss  40281  nneop  40386  fldivexpfllog2  40429  digexp  40471
  Copyright terms: Public domain W3C validator