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

Theorem biimpri 199
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 195 . 2  |-  ( ps  <->  ph )
32biimpi 188 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178
This theorem is referenced by:  mpbir  202  sylibr  205  sylbir  206  syl5bir  211  syl6ibr  220  bitri  242  mtbi  291  pm2.54  365  sylanbr  461  sylan2br  464  pm3.11  487  orbi2i  507  pm2.31  513  simplbi2  610  dfbi  612  pm2.85  828  rnlem  933  syl3an1br  1223  syl3an2br  1224  syl3an3br  1225  3impexpbicom  1359  nic-axALT  1430  sbbii  1636  hbn1fw  1680  equveli  1930  exmoeu  2186  eueq2  2940  ralun  3358  ssunieq  3861  ax9vsep  4146  ordunidif  4439  unizlim  4508  dfwe2  4572  onminex  4597  nnsuc  4672  opelxpi  4720  ndmima  5049  dffo2  5420  dff1o2  5442  resdif  5459  f1o00  5473  fvimacnvALT  5605  exfo  5639  ressnop0  5664  fsnunfv  5681  ovid  5925  ovidig  5926  f1stres  6102  f2ndres  6103  1st2val  6106  2nd2val  6107  frxp  6186  soxp  6189  tz7.49  6452  abianfp  6466  elixpsn  6850  domdifsn  6940  domunsncan  6957  fineqvlem  7072  unblem4  7107  ordiso2  7225  domwdom  7283  inf3lem3  7326  trcl  7405  unir1  7480  ssrankr1  7502  pm54.43lem  7627  infxpenlem  7636  ween  7657  acni3  7669  kmlem1  7771  infdif  7830  ackbij1lem1  7841  fin23lem14  7954  fin23lem32  7965  fin23lem40  7972  isfin1-3  8007  axcc2lem  8057  axdc3lem2  8072  axcclem  8078  ac6c4  8103  zornn0g  8127  axdclem2  8142  brdom3  8148  brdom5  8149  brdom4  8150  brdom6disj  8152  konigthlem  8185  pwcfsdom  8200  cfpwsdom  8201  alephom  8202  gruina  8435  grur1  8437  grothomex  8446  grothac  8447  nqpr  8633  axcnre  8781  axpre-sup  8786  ssxr  8887  le2tri3i  8944  0nn0  9975  uzind4  10271  rpnnen1lem5  10341  elfz4  10785  eluzfz  10787  hashxplem  11379  hashfun  11383  ccatswrd  11453  resqrex  11730  ndvdsadd  12601  gcdcllem1  12684  gcdcllem3  12686  1idssfct  12758  xpsff1o  13464  xpsmnd  14406  xpsgrp  14608  odlem1  14844  gexlem1  14884  dprdfeq0  15251  gsumdixp  15386  lspcl  15727  tgcl  16701  elcls  16804  opnnei  16851  cnpnei  16987  cmpcov2  17111  cmpfii  17130  txcnp  17308  xpstps  17495  fbun  17529  isfild  17547  snfil  17553  filcon  17572  isufil2  17597  hauspwpwf1  17676  xpsxms  18074  xpsms  18075  rlmnvc  18207  nmoid  18245  xrsmopn  18312  xrhmeo  18438  cphsqrcl  18614  iscmet3  18713  iundisj  18899  ioorinv  18925  plyexmo  19687  aalioulem3  19708  dvtaylp  19743  dvradcnv  19791  logtayllem  20000  logtayl  20001  musum  20425  pntlem3  20752  subgoablo  20970  ismndo2  21004  rngomndo  21080  sspval  21291  blo3i  21372  ajfval  21379  spanval  21904  cmcmlem  22162  cnvbraval  22682  leopnmid  22710  csmdsymi  22906  chirredlem4  22965  sumdmdlem  22990  ballotlemsdom  23063  ballotlemsel1i  23064  ballotlemsima  23067  ballotlemro  23074  ballotlemfrcn0  23081  ballotth  23089  cvmsdisj  23205  climuzcnv  23408  dfon2lem3  23542  dfon2lem7  23546  sspred  23575  sltval2  23710  axdenselem5  23740  imageval  23876  df3nandALT1  24242  lukshef-ax2  24261  arg-ax  24262  bibox  24380  binxt  24382  bidia  24387  evpexun  24396  difeqri2  24438  twsymr  24476  celsor  24509  dstr  24570  fisub  24953  cndpv  25448  gltpntl2  25472  xsyysx  25544  bsstrs  25545  nbssntrs  25546  pdiveql  25567  filnetlem2  25727  heiborlem3  25936  isfld2  26029  igenval2  26090  isfldidl  26092  dmncan2  26101  pellexlem5  26317  rmyabs  26444  jm2.24  26449  islssfgi  26569  pwslnm  26595  lindfind  26685  lindsind  26686  lindsind2  26688  lindff1  26689  f1linds  26694  islindf4  26707  dgraaub  26752  gsumcom3fi  26854  infrglb  27121  stoweidlem14  27162  stoweidlem15  27163  stoweidlem17  27165  stoweidlem35  27183  stoweidlem55  27203  stoweidlem57  27205  stoweidlem58  27206  stoweidlem59  27207  stoweid  27211  stirlinglem7  27228  stirlinglem10  27231  stirlinglem12  27233  fnresfnco  27362  dfdfat2  27369  afvres  27411  ndmaovass  27445  logbid1  27527  ee3bir  27535  vk15.4j  27562  onfrALTlem2  27582  a9e2nd  27595  dfvd1impr  27616  dfvd2impr  27644  e1bir  27670  e2bir  27673  e3bir  27782  19.21a3con13vVD  27896  3impexpbicomVD  27901  tratrbVD  27905  ssralv2VD  27910  truniALTVD  27922  trintALTVD  27924  undif3VD  27926  onfrALTlem3VD  27931  onfrALTlem2VD  27933  onfrALTVD  27935  relopabVD  27945  a9e2ndVD  27952  2uasbanhVD  27955  vk15.4jVD  27958  sspwimp  27962  sspwimpVD  27963  sspwimpcf  27964  sspwimpcfVD  27965  suctrALTcf  27966  suctrALTcfVD  27967  suctrALT3  27968  sspwimpALT  27969  unisnALT  27970  suctrALT4  27972  sspwimpALT2  27973  a9e2ndALT  27975  bnj1136  28294  bnj1175  28301  bnj1408  28333  ax12OLD  28372  a12lem1  28397  lsat0cv  28490  pclfinclN  29406  docavalN  30580  djavalN  30592  dochval  30808  djhval  30855  dochexmidlem8  30924  dochkr1  30935  dochkr1OLDN  30936  hdmap1fval  31254
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator