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

Theorem biimprd 226
Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 201 and biimpri 209. (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 23 . 2  |-  ( ch 
->  ch )
2 biimprd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5ibr 224 1  |-  ( ph  ->  ( ch  ->  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:  syl6bir  232  mpbird  235  sylibrd  237  sylbird  238  con4bid  294  mtbid  301  mtbii  303  imbi1d  318  biimpar  487  prlem1  970  spfw  1856  cbvalw  1858  alcomiw  1861  ax12v  1906  nfimd  1973  axc11nlem  1994  cbval  2075  axc11nlemOLD  2103  axc16i  2119  equvini  2142  axc16gALT  2159  sbequi  2169  eqrdav  2420  cleqhOLD  2538  pm13.18  2735  rspcimdv  3183  rspcedv  3186  moi2  3252  moi  3254  eqrd  3482  sspsstr  3570  eqoreldif  4038  ralxfrd  4632  ralxfr2d  4634  isso2i  4803  wefrc  4844  elres  5156  sotri3  5246  oneqmini  5490  ordsssuc2  5527  ordtri2or  5534  2elresin  5702  f1ocnv  5840  tz6.12c  5897  fveqres  5912  fvun1  5949  dffo4  6050  fconst5  6134  fnprb  6135  isores3  6238  f1owe  6256  weniso  6257  ndmovordi  6471  orduniorsuc  6668  ordzsl  6683  tfinds  6697  f1oweALT  6788  fnse  6921  tposfo2  7001  wfrlem5  7045  wfrlem12  7052  issmo2  7073  iordsmo  7081  smoel2  7087  tz7.48lem  7163  oawordeulem  7260  om00  7281  omlimcl  7284  odi  7285  nnawordi  7327  fiint  7851  fipreima  7883  dffi2  7940  suplub2  7978  wemapsolem  8068  unwdomg  8102  inf3lem3  8138  trcl  8214  fidomtri  8429  prdom2  8439  cardaleph  8521  ackbij1lem16  8666  coflim  8692  coftr  8704  infpssrlem4  8737  isfin7-2  8827  axdc3lem2  8882  axdc3lem4  8884  brdom6disj  8961  entric  8983  fpwwe2lem12  9067  inatsk  9204  grur1a  9245  indpi  9333  reclem3pr  9475  supsrlem  9536  lelttr  9725  dedekindle  9799  negn0  10049  fimaxre  10552  nnmulcl  10633  arch  10867  nnnegz  10941  zeo  11022  uzm1  11190  rpneg  11333  xrlttri  11439  xrlelttr  11454  iccid  11682  icoshft  11755  fzen  11817  elfz2nn0  11886  elfzom1p1elfzo  11993  fleqceilz  12081  zmodidfzoimp  12127  hasheqf1oi  12534  hashnfinnn0  12542  swrd0  12781  swrdccatin12lem2  12836  swrdccat  12840  swrdccat3blem  12842  repswswrd  12878  trclublem  13048  max0add  13362  abslt  13366  absle  13367  rexuzre  13404  caurcvg  13730  caurcvgOLD  13731  caucvg  13733  dvdsval2  14296  negdvdsb  14307  muldvds2  14316  smuval2  14444  smupvallem  14445  rplpwr  14512  alginv  14522  algfx  14527  prmgt1  14631  coprmgcdb  14642  rpexp1i  14661  qnumdencl  14676  phiprmpw  14712  prmdiveq  14722  pcmpt  14825  infpnlem1  14842  prmgaplem3  15011  prmgaplem8  15016  imasaddfnlem  15422  plelttr  16206  lubval  16218  lublecllem  16222  glbval  16231  mrcmndind  16601  mndodconglem  17178  elfrlmbasn0  19312  mavmulsolcl  19563  slesolex  19694  fvmptnn04if  19860  chfacfisf  19865  chfacfisfcpmat  19866  cnpnei  20267  uncon  20431  comppfsc  20534  kqsat  20733  isr0  20739  qtophmeo  20819  trufil  20912  alexsubALT  21053  cnextcn  21069  ucnima  21283  iducn  21285  bl2in  21402  addcnlem  21883  rescncf  21916  ovoliunlem2  22443  voliun  22494  mbflimsup  22610  mbflimsupOLD  22611  itgcn  22787  dvdsq1p  23098  aalioulem2  23276  recosf1o  23471  logrec  23687  xrlimcnp  23881  basellem4  23997  bposlem1  24199  bposlem5  24203  lgsdchrval  24262  pntlem3  24434  brbtwn2  24922  axbtwnid  24956  usgraedgprv  25090  usgraedgrnv  25091  usgrafisinds  25127  iswlkg  25238  wwlkextinj  25444  isclwlkg  25469  clwlkisclwwlklem2a1  25493  clwwisshclww  25521  clwlksizeeq  25566  eupai  25681  numclwwlkovf2ex  25800  numclwwlk2lem1  25816  numclwwlk5lem  25825  frgrareggt1  25830  friendship  25836  elghomlem2OLD  26076  blocn2  26435  htthlem  26556  axhcompl-zf  26637  spanuni  27183  spansncol  27207  spansneleq  27209  elspansn5  27213  idcnop  27620  pjnormssi  27807  dmdmd  27939  bian1d  28086  ifeqeqx  28148  supxrnemnf  28348  rexdiv  28390  xrstos  28436  xrge0omnd  28469  cnre2csqlem  28712  fsumcvg4  28752  lmxrge0  28754  qqhval2lem  28781  esumpr2  28884  esumcvg  28903  issgon  28941  measxun2  29028  measres  29040  measdivcstOLD  29042  measdivcst  29043  elorrvc  29292  signsply0  29436  bnj580  29720  erdsze2lem2  29923  cvmsval  29985  ghomgsg  30307  ghomf1olem  30308  fundmpss  30402  dfon2lem3  30426  frmin  30475  poseq  30486  soseq  30487  frrlem5  30513  frrlem11  30521  nobndup  30582  nobnddown  30583  dfrdg4  30711  cgrtriv  30762  btwntriv2  30772  ifscgr  30804  lineext  30836  btwnconn1lem12  30858  colinbtwnle  30878  elicc3  30966  ontgval  31084  onsucconi  31090  bj-bibibi  31162  bj-cbvexw  31223  bj-cbvalv  31284  bj-axc11nlemv  31302  bj-cleqh  31345  bj-equsal  31386  bj-elid  31591  bj-finsumval0  31654  relowlssretop  31707  wl-nfs1t  31785  wl-ax12v2  31823  finixpnum  31844  ltflcei  31847  poimirlem23  31877  poimirlem24  31878  poimirlem27  31881  poimirlem32  31886  itg2addnclem  31907  areacirclem2  31947  areacirclem5  31950  areacirc  31951  nninfnub  31994  prdstotbnd  32040  heiborlem4  32060  heibor  32067  grpokerinj  32097  isidlc  32162  prtlem17  32366  dral1-o  32393  axc16g-o  32424  lsator0sp  32486  atlrelat1  32806  cvratlem  32905  diaintclN  34545  dibintclN  34654  cdlemn11pre  34697  dihord2pre  34712  dihintcl  34831  dochkrshp4  34876  lcfrlem9  35037  lcfrlem21  35050  mapdh8e  35271  elrfirn2  35457  rencldnfilem  35582  sdrgacs  35987  intimasn  36109  ss2iundf  36111  ov2ssiunov2  36152  comptiunov2i  36158  iunrelexpuztr  36171  snelpwrVD  37088  en3lplem1VD  37100  en3lpVD  37102  orbi1rVD  37105  sbc3orgVD  37108  3impexpVD  37113  equncomVD  37126  trsbcVD  37135  trintALTVD  37138  trintALT  37139  csbingVD  37142  csbsngVD  37151  csbxpgVD  37152  csbrngVD  37154  csbfv12gALTVD  37157  relopabVD  37159  e2ebindVD  37170  stoweidlem35  37716  stoweidlem48  37729  rexrsb  38303  funbrafv  38372  rlimdmafv  38391  fzopredsuc  38432  iccpartlt  38450  nnsum3primesle9  38601  wtgoldbnnsum4prm  38609  bgoldbnnsum3prm  38611  pfxccatin12lem2  38677  funopsn  38717  fzoopth  38752  2ffzoeq  38753  usgredgprv  38908  usgedgvadf1lem2  38998  usgedgvadf1ALTlem2  39001  usgfis  39030  usgfisALT  39034  usgrafiedgALT  39035  mgm2mgm  39135  2zrngnmlid  39221  2zrngnmrid  39222  ellcoellss  39502  nneop  39607  fldivexpfllog2  39650  digexp  39692
  Copyright terms: Public domain W3C validator