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

Theorem biimpri 197
Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
Hypothesis
Ref Expression
biimpri.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
biimpri  |-  ( ps 
->  ph )

Proof of Theorem biimpri
StepHypRef Expression
1 biimpri.1 . . 3  |-  ( ph  <->  ps )
21bicomi 193 . 2  |-  ( ps  <->  ph )
32biimpi 186 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  mpbir  200  sylibr  203  sylbir  204  syl5bir  209  syl6ibr  218  bitri  240  mtbi  289  pm2.54  363  sylanbr  459  sylan2br  462  pm3.11  485  orbi2i  505  pm2.31  511  simplbi2  608  dfbi  610  pm2.85  826  rnlem  931  syl3an1br  1221  syl3an2br  1222  syl3an3br  1223  3impexpbicom  1357  nic-axALT  1429  sbbii  1634  hbn1fw  1679  equveli  1928  exmoeu  2185  eueq2  2939  ralun  3357  ssunieq  3860  ax9vsep  4145  ordunidif  4440  unizlim  4509  dfwe2  4573  onminex  4598  nnsuc  4673  opelxpi  4721  ndmima  5050  dffo2  5455  dff1o2  5477  resdif  5494  f1o00  5508  fvimacnvALT  5644  exfo  5678  ressnop0  5703  fsnunfv  5720  ovid  5964  ovidig  5965  f1stres  6141  f2ndres  6142  1st2val  6145  2nd2val  6146  frxp  6225  soxp  6228  tz7.49  6457  abianfp  6471  elixpsn  6855  domdifsn  6945  domunsncan  6962  fineqvlem  7077  unblem4  7112  ordiso2  7230  domwdom  7288  inf3lem3  7331  trcl  7410  unir1  7485  ssrankr1  7507  pm54.43lem  7632  infxpenlem  7641  ween  7662  acni3  7674  kmlem1  7776  infdif  7835  ackbij1lem1  7846  fin23lem14  7959  fin23lem32  7970  fin23lem40  7977  isfin1-3  8012  axcc2lem  8062  axdc3lem2  8077  axcclem  8083  ac6c4  8108  zornn0g  8132  axdclem2  8147  brdom3  8153  brdom5  8154  brdom4  8155  brdom6disj  8157  konigthlem  8190  pwcfsdom  8205  cfpwsdom  8206  alephom  8207  gruina  8440  grur1  8442  grothomex  8451  grothac  8452  nqpr  8638  axcnre  8786  axpre-sup  8791  ssxr  8892  le2tri3i  8949  0nn0  9980  uzind4  10276  rpnnen1lem5  10346  elfz4  10791  eluzfz  10793  hashxplem  11385  hashfun  11389  ccatswrd  11459  resqrex  11736  ndvdsadd  12607  gcdcllem1  12690  gcdcllem3  12692  1idssfct  12764  xpsff1o  13470  xpsmnd  14412  xpsgrp  14614  odlem1  14850  gexlem1  14890  dprdfeq0  15257  gsumdixp  15392  lspcl  15733  tgcl  16707  elcls  16810  opnnei  16857  cnpnei  16993  cmpcov2  17117  cmpfii  17136  txcnp  17314  xpstps  17501  fbun  17535  isfild  17553  snfil  17559  filcon  17578  isufil2  17603  hauspwpwf1  17682  xpsxms  18080  xpsms  18081  rlmnvc  18213  nmoid  18251  xrsmopn  18318  xrhmeo  18444  cphsqrcl  18620  iscmet3  18719  iundisj  18905  ioorinv  18931  plyexmo  19693  aalioulem3  19714  dvtaylp  19749  dvradcnv  19797  logtayllem  20006  logtayl  20007  musum  20431  pntlem3  20758  subgoablo  20978  ismndo2  21012  rngomndo  21088  sspval  21299  blo3i  21380  ajfval  21387  spanval  21912  cmcmlem  22170  cnvbraval  22690  leopnmid  22718  csmdsymi  22914  chirredlem4  22973  sumdmdlem  22998  ballotlemsdom  23070  ballotlemsel1i  23071  ballotlemsima  23074  ballotlemro  23081  ballotlemfrcn0  23088  ballotth  23096  cvmsdisj  23212  climuzcnv  23415  dfon2lem3  23552  dfon2lem7  23556  sspred  23585  sltval2  23721  nodenselem5  23750  imageval  23880  df3nandALT1  24246  lukshef-ax2  24265  arg-ax  24266  bibox  24394  binxt  24396  bidia  24401  evpexun  24410  difeqri2  24452  twsymr  24490  celsor  24523  dstr  24583  fisub  24966  cndpv  25461  gltpntl2  25485  xsyysx  25557  bsstrs  25558  nbssntrs  25559  pdiveql  25580  filnetlem2  25740  heiborlem3  25949  isfld2  26042  igenval2  26103  isfldidl  26105  dmncan2  26114  pellexlem5  26330  rmyabs  26457  jm2.24  26462  islssfgi  26582  pwslnm  26608  lindfind  26698  lindsind  26699  lindsind2  26701  lindff1  26702  f1linds  26707  islindf4  26720  dgraaub  26765  gsumcom3fi  26867  infrglb  27134  stoweidlem14  27175  stoweidlem15  27176  stoweidlem17  27178  stoweidlem35  27196  stoweidlem55  27216  stoweidlem57  27218  stoweidlem58  27219  stoweidlem59  27220  stoweid  27224  stirlinglem7  27241  stirlinglem10  27244  stirlinglem12  27246  fnresfnco  27401  dfdfat2  27406  afvres  27446  ndmaovass  27478  frgra0v  27536  logbid1  27629  ee3bir  27637  vk15.4j  27664  onfrALTlem2  27684  a9e2nd  27697  dfvd1impr  27718  dfvd2impr  27749  e1bir  27775  e2bir  27778  e3bir  27887  19.21a3con13vVD  28001  3impexpbicomVD  28006  tratrbVD  28010  ssralv2VD  28015  truniALTVD  28027  trintALTVD  28029  undif3VD  28031  onfrALTlem3VD  28036  onfrALTlem2VD  28038  onfrALTVD  28040  relopabVD  28050  a9e2ndVD  28057  2uasbanhVD  28060  vk15.4jVD  28063  sspwimp  28067  sspwimpVD  28068  sspwimpcf  28069  sspwimpcfVD  28070  suctrALTcf  28071  suctrALTcfVD  28072  suctrALT3  28073  sspwimpALT  28074  unisnALT  28075  suctrALT4  28077  sspwimpALT2  28078  a9e2ndALT  28080  bnj1136  28400  bnj1175  28407  bnj1408  28439  ax12OLD  28478  a12lem1  28503  lsat0cv  28596  pclfinclN  29512  docavalN  30686  djavalN  30698  dochval  30914  djhval  30961  dochexmidlem8  31030  dochkr1  31041  dochkr1OLDN  31042  hdmap1fval  31360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator