Theorem biimpri 231

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 223. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)

Hypothesis

Ref	Expression
biimpri.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
biimpri	⊢ (𝜓 → 𝜑)

Proof of Theorem biimpri

Step	Hyp	Ref	Expression
1		biimpri.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	bicomi 227	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 219	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  mpbir  234  sylibr  237  sylbir  238  sylbbr  239  sylbb1  240  sylbb2  241  syl5bir  246  syl6ibr  255  mtbi  325  sylnib  331  simplbi2  504  sylanbr  585  sylan2br  597  pm2.54  849  orbi2i  910  pm2.31  920  pm2.85  930  pm3.11  990  syl3an1br  1403  syl3an2br  1404  syl3an3br  1405  had1  1605  nic-axALT  1676  speimfw  1966  sbbii  2081  sb2vOLD  2094  hbsbw  2173  sbbiiALT  2554  mobii  2606  mo4  2625  nfabdw  2976  r19.30  3293  ceqsexv2d  3490  eueq2  3649  ralun  4119  ssunieq  4835  ax6vsep  5171  opelxpi  5556  ordunidif  6207  unizlim  6275  dffo2  6569  dff1o2  6595  resdif  6610  f1o00  6624  fvimacnvALT  6804  fvcofneq  6836  exfo  6848  ressnop0  6892  fsnunfv  6926  ovid  7270  ovidig  7271  dfwe2  7476  onminex  7502  nnsuc  7577  1stnpr  7675  2ndnpr  7676  f1stres  7695  f2ndres  7696  1st2val  7699  2nd2val  7700  frxp  7803  soxp  7806  tz7.49  8064  elixpsn  8484  domdifsn  8583  domunsncan  8600  fineqvlem  8716  unblem4  8757  ordiso2  8963  zfreg  9043  inf3lem3  9077  trcl  9154  unir1  9226  ssrankr1  9248  djuunxp  9334  pm54.43lem  9413  infxpenlem  9424  ween  9446  acni3  9458  kmlem1  9561  infdif  9620  ackbij1lem1  9631  fin23lem32  9755  isfin1-3  9797  axdc3lem2  9862  ac6c4  9892  zornn0g  9916  axdclem2  9931  rnct  9936  brdom3  9939  brdom5  9940  brdom4  9941  brdom6disj  9943  konigthlem  9979  pwcfsdom  9994  cfpwsdom  9995  alephom  9996  gruina  10229  grur1  10231  grothomex  10240  grothac  10241  nqpr  10425  axcnre  10575  axpre-sup  10580  ssxr  10699  le2tri3i  10759  muldivdir  11322  0nn0  11900  uzind4  12294  rpnnen1lem5  12368  elfz4  12895  eluzfz  12897  ssfzo12bi  13127  hashgt0elex  13758  hashgt23el  13781  hashxplem  13790  hashfun  13794  ishashinf  13817  wrdsymb1  13896  ccatfv0  13928  lswccats1fst  13985  ccatswrd  14021  ccatpfx  14054  splfv1  14108  repswfsts  14134  cshinj  14164  swrdco  14190  cotr2g  14327  trclun  14365  resqrex  14602  pwm1geoserOLD  15217  sumeven  15728  ndvdsadd  15751  gcdcllem1  15838  gcdcllem3  15840  lcmftp  15970  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  divgcdcoprmex  16000  1idssfct  16014  prmodvdslcmf  16373  cshwrepswhash1  16428  xpsfrnel2  16829  xpsff1o  16832  initoeu2  17268  clatlem  17713  clatlubcl2  17715  clatglbcl2  17717  xpsmnd  17943  xpsgrp  18210  mulgfval  18218  gsmsymgrfix  18548  pmtr3ncom  18595  gsumcom3fi  19092  dprdfeq0  19137  gsumdixp  19355  lspcl  19741  lindfind  20505  lindsind  20506  lindsind2  20508  lindff1  20509  f1linds  20514  mat1dimscm  21080  mdetunilem7  21223  fvmptnn04if  21454  tgcl  21574  elcls  21678  opnnei  21725  neiptopnei  21737  cnpnei  21869  cmpfii  22014  txcnp  22225  xpstps  22415  fbun  22445  isfild  22463  snfil  22469  filconn  22488  isufil2  22513  hauspwpwf1  22592  cnextcn  22672  ustfilxp  22818  ustuqtop4  22850  xpsxms  23141  xpsms  23142  rlmnvc  23309  nmoid  23348  xrsmopn  23417  xrhmeo  23551  cphsqrtcl  23789  iscmet3  23897  iundisj  24152  ioorinv  24180  bddiblnc  24445  dvtaylp  24965  logbid1  25354  logbchbase  25357  relogbcxpb  25373  logbmpt  25374  logbfval  25376  musum  25776  lgsmodeq  25926  lgsmulsqcoprm  25927  2lgs  25991  2sqnn0  26022  pntlem3  26193  nbupgrel  27135  nbusgrvtxm1  27169  nb3gr2nb  27174  pthdivtx  27518  pthdlem2lem  27556  crctisclwlk  27583  wwlks  27621  wwlksonvtx  27641  wspthnonp  27645  wlkiswwlks2lem1  27655  wwlksnndef  27691  wwlksnfi  27692  clwlkclwwlkf1lem3  27791  clwlkclwwlkf1  27795  clwwlknnn  27818  clwwlkel  27831  clwwlkf1  27834  wwlksext2clwwlk  27842  clwwlknonwwlknonb  27891  umgr3v3e3cycl  27969  frgrncvvdeq  28094  sspval  28506  blo3i  28585  ajfval  28592  spanval  29116  cmcmlem  29374  leopnmid  29921  csmdsymi  30117  chirredlem4  30176  sumdmdlem  30201  iundisjf  30352  padct  30481  iundisjfi  30545  hashxpe  30555  fprodex01  30567  xrpxdivcld  30637  wrdt2ind  30653  lsmsnorb  30999  mxidlnzr  31047  extdgval  31132  ccfldextdgrr  31145  pnfneige0  31304  rrhre  31372  esumcocn  31449  hasheuni  31454  sgon  31493  sigapildsys  31531  ddemeas  31605  dya2iocct  31648  dya2iocnrect  31649  eulerpartgbij  31740  eulerpartlemgs2  31748  coinflippv  31851  signstfvneq0  31952  hgt750lemb  32037  bnj1136  32379  bnj1175  32386  bnj1408  32418  fnrelpredd  32472  pthhashvtx  32487  spthcycl  32489  upgracycumgr  32513  umgracycusgr  32514  cvmsdisj  32630  mrsubvrs  32882  mppspstlem  32931  problem4  33024  climuzcnv  33027  dford5  33070  dfon2lem7  33147  fprlem1  33250  sltval2  33276  noxp1o  33283  conway  33377  scutbdaylt  33389  imageval  33504  filnetlem2  33840  df3nandALT1  33860  lukshef-ax2  33876  arg-ax  33877  bj-andnotim  34035  bj-modalbe  34135  bj-hbs1  34249  bj-hbsb2av  34251  bj-2uplex  34458  mptsnunlem  34755  onsucuni3  34784  fvineqsneq  34829  finixpnum  35042  fin2solem  35043  matunitlindflem2  35054  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  poimirlem32  35089  mblfinlem3  35096  itg2addnclem2  35109  itg2addnc  35111  ftc1anclem6  35135  heiborlem3  35251  ismndo2  35312  rngomndo  35373  isfld2  35443  isfldidl  35506  dmncan2  35515  oprabbi  35599  opabbi  35603  ac6s3f  35609  relcnveq3  35738  elrelscnveq3  35891  lsat0cv  36329  pclfinclN  37246  docavalN  38419  djavalN  38431  dochval  38647  djhval  38694  dochexmidlem8  38763  dochkr1  38774  dochkr1OLDN  38775  hdmap1fval  39092  lcmineqlem13  39329  selvval2lem5  39432  pellexlem5  39774  rmyabs  39899  jm2.24  39904  islssfgi  40016  pwslnm  40038  dgraaub  40092  ensucne0OLD  40238  iscard5  40242  clrellem  40322  frege114d  40459  frege55lem1a  40567  frege70  40634  gneispace  40837  3impexpbicom  41185  ee3bir  41209  vk15.4j  41234  onfrALTlem2  41252  ax6e2nd  41264  dfvd1impr  41282  dfvd2impr  41310  e1bir  41336  e2bir  41339  e3bir  41445  suctrALT  41532  19.21a3con13vVD  41558  3impexpbicomVD  41563  tratrbVD  41567  ssralv2VD  41572  truniALTVD  41584  trintALTVD  41586  undif3VD  41588  onfrALTlem3VD  41593  onfrALTlem2VD  41595  onfrALTVD  41597  relopabVD  41607  ax6e2ndVD  41614  2uasbanhVD  41617  vk15.4jVD  41620  sspwimp  41624  sspwimpVD  41625  sspwimpcf  41626  sspwimpcfVD  41627  suctrALTcf  41628  suctrALTcfVD  41629  suctrALT3  41630  sspwimpALT  41631  unisnALT  41632  ax6e2ndALT  41636  isosctrlem1ALT  41640  iunconnlem2  41641  supminfxrrnmpt  42110  limsuppnflem  42352  limsupubuz  42355  cncfuni  42528  iblcncfioo  42620  stoweidlem14  42656  stoweidlem17  42659  stoweidlem35  42677  stoweidlem57  42699  stirlinglem7  42722  stirlinglem10  42725  fourierdlem54  42802  fourierdlem62  42810  fourierdlem63  42811  fourierdlem65  42813  fourierdlem73  42821  fourierdlem80  42828  fourierdlem82  42830  fourierdlem101  42849  etransclem32  42908  ioorrnopnxr  42949  subsaliuncl  42998  meadjiunlem  43104  ismeannd  43106  voliunsge0lem  43111  volmea  43113  caratheodory  43167  ovnsubaddlem2  43210  hoidmvlelem5  43238  hoiqssbllem2  43262  iinhoiicc  43313  aibandbiaiaiffb  43488  funressnvmo  43637  dfdfat2  43684  afvres  43728  tz6.12-afv  43729  ndmaovass  43762  afv2res  43795  tz6.12-afv2  43796  el1fzopredsuc  43882  fzoopth  43884  fundcmpsurinjimaid  43928  iccpartiltu  43939  iccelpart  43950  lswn0  43961  ichnfimlem  43980  prprelb  44033  evenprm2  44232  lincext1  44863