Theorem biimpri 228

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 220. (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 224	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 216	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  mpbir  231  sylibr  234  sylbir  235  sylbbr  236  sylbb1  237  sylbb2  238  biimtrrid  243  imbitrrdi  252  mtbi  322  sylnib  328  simplbi2  500  sylanbr  582  sylan2br  595  pm2.54  852  orbi2i  912  pm2.31  922  pm2.85  932  pm3.11  994  syl3an1br  1405  syl3an2br  1406  syl3an3br  1407  had1  1599  nic-axALT  1670  speimfw  1960  sbbii  2073  hbsbwOLD  2169  mobii  2545  mo4  2563  r19.30  3117  r19.30OLD  3118  ceqsexv2dOLD  3533  eueq2  3718  ralun  4207  ssunieq  4947  ax6vsep  5308  opelxpi  5725  ordunidif  6434  unizlim  6508  dffo2  6824  dff1o2  6853  resdif  6869  f1o00  6883  fvimacnvALT  7076  fvcofneq  7112  exfo  7124  ressnop0  7172  fsnunfv  7206  ovid  7573  ovidig  7574  dfwe2  7792  dford5  7802  onminex  7821  nnsuc  7904  1stnpr  8016  2ndnpr  8017  f1stres  8036  f2ndres  8037  1st2val  8040  2nd2val  8041  frxp  8149  soxp  8152  frxp2  8167  fprlem1  8323  tz7.49  8483  elixpsn  8975  domdifsn  9092  domunsncan  9110  unfi  9209  cnvfi  9214  fineqvlem  9295  unblem4  9328  ordiso2  9552  zfreg  9632  inf3lem3  9667  trcl  9765  unir1  9850  ssrankr1  9872  djuunxp  9958  pm54.43lem  10037  infxpenlem  10050  ween  10072  acni3  10084  kmlem1  10188  infdif  10245  ackbij1lem1  10256  fin23lem32  10381  isfin1-3  10423  axdc3lem2  10488  ac6c4  10518  zornn0g  10542  axdclem2  10557  rnct  10562  brdom3  10565  brdom5  10566  brdom4  10567  brdom6disj  10569  konigthlem  10605  pwcfsdom  10620  cfpwsdom  10621  alephom  10622  gruina  10855  grur1  10857  grothomex  10866  grothac  10867  nqpr  11051  axcnre  11201  axpre-sup  11206  ssxr  11327  le2tri3i  11388  muldivdir  11957  0nn0  12538  uzind4  12945  rpnnen1lem5  13020  elfz4  13553  eluzfz  13555  ssfzo12bi  13796  fzoopth  13797  hashgt0elex  14436  hashgt23el  14459  hashxplem  14468  hashfun  14472  ishashinf  14498  wrdsymb1  14587  ccatfv0  14617  lswccats1fst  14669  ccatswrd  14702  ccatpfx  14735  splfv1  14789  repswfsts  14815  cshinj  14845  swrdco  14872  cotr2g  15011  trclun  15049  resqrex  15285  sumeven  16420  ndvdsadd  16443  gcdcllem1  16532  gcdcllem3  16534  lcmftp  16669  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfun  16678  coprmprod  16694  coprmproddvdslem  16695  divgcdcoprmex  16699  1idssfct  16713  prmodvdslcmf  17080  cshwrepswhash1  17136  xpsfrnel2  17610  xpsff1o  17613  catcone0  17731  initoeu2  18069  clatlem  18559  clatlubcl2  18561  clatglbcl2  18563  xpsmnd  18802  xpsgrp  19089  mulgfval  19099  gsmsymgrfix  19460  pmtr3ncom  19507  gsumcom3fi  20011  dprdfeq0  20056  gsumdixp  20332  lspcl  20991  lindfind  21853  lindsind  21854  lindsind2  21856  lindff1  21857  f1linds  21862  evls1maplmhm  22396  mat1dimscm  22496  mdetunilem7  22639  fvmptnn04if  22870  tgcl  22991  elcls  23096  opnnei  23143  neiptopnei  23155  cnpnei  23287  cmpfii  23432  txcnp  23643  xpstps  23833  fbun  23863  isfild  23881  snfil  23887  filconn  23906  isufil2  23931  hauspwpwf1  24010  cnextcn  24090  ustfilxp  24236  ustuqtop4  24268  xpsxms  24562  xpsms  24563  rlmnvc  24739  nmoid  24778  xrsmopn  24847  xrhmeo  24990  cphsqrtcl  25231  iscmet3  25340  iundisj  25596  ioorinv  25624  bddiblnc  25891  dvtaylp  26426  logbid1  26825  logbchbase  26828  relogbcxpb  26844  logbmpt  26845  logbfval  26847  musum  27248  lgsmodeq  27400  lgsmulsqcoprm  27401  2lgs  27465  2sqnn0  27496  pntlem3  27667  sltval2  27715  noxp1o  27722  conway  27858  scutbdaylt  27877  nbupgrel  29376  nbusgrvtxm1  29410  nb3gr2nb  29415  pthdivtx  29761  pthdlem2lem  29799  crctisclwlk  29826  wwlks  29864  wwlksonvtx  29884  wspthnonp  29888  wlkiswwlks2lem1  29898  wwlksnndef  29934  wwlksnfi  29935  clwlkclwwlkf1lem3  30034  clwlkclwwlkf1  30038  clwwlknnn  30061  clwwlkel  30074  clwwlkf1  30077  wwlksext2clwwlk  30085  clwwlknonwwlknonb  30134  umgr3v3e3cycl  30212  frgrncvvdeq  30337  sspval  30751  blo3i  30830  ajfval  30837  spanval  31361  cmcmlem  31619  leopnmid  32166  csmdsymi  32362  chirredlem4  32421  sumdmdlem  32446  iundisjf  32608  padct  32736  iundisjfi  32803  nn0difffzod  32813  hashxpe  32816  fprodex01  32831  xrpxdivcld  32901  gsumfs2d  33040  fldgensdrg  33295  lsmsnorb  33398  mxidlnzr  33474  zringfrac  33561  lactlmhm  33661  extdgval  33681  ccfldextdgrr  33696  ply1annprmidl  33714  pnfneige0  33911  rrhre  33983  esumcocn  34060  hasheuni  34065  sgon  34104  sigapildsys  34142  ddemeas  34216  dya2iocct  34261  dya2iocnrect  34262  eulerpartgbij  34353  eulerpartlemgs2  34361  coinflippv  34464  signstfvneq0  34565  hgt750lemb  34649  bnj1136  34989  bnj1175  34996  bnj1408  35028  fnrelpredd  35081  pthhashvtx  35111  spthcycl  35113  upgracycumgr  35137  umgracycusgr  35138  cvmsdisj  35254  mrsubvrs  35506  mppspstlem  35555  problem4  35652  climuzcnv  35655  currybi  35672  dfon2lem7  35770  imageval  35911  filnetlem2  36361  df3nandALT1  36381  lukshef-ax2  36397  arg-ax  36398  weiunpo  36447  bj-andnotim  36570  bj-modalbe  36670  bj-hbs1  36794  bj-hbsb2av  36796  bj-2uplex  37004  mptsnunlem  37320  onsucuni3  37349  fvineqsneq  37394  finixpnum  37591  fin2solem  37592  matunitlindflem2  37603  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem32  37638  mblfinlem3  37645  itg2addnclem2  37658  itg2addnc  37660  ftc1anclem6  37684  heiborlem3  37799  ismndo2  37860  rngomndo  37921  isfld2  37991  isfldidl  38054  dmncan2  38063  oprabbi  38147  opabbi  38151  ac6s3f  38157  relcnveq3  38302  elrelscnveq3  38472  lsat0cv  39014  pclfinclN  39932  docavalN  41105  djavalN  41117  dochval  41333  djhval  41380  dochexmidlem8  41449  dochkr1  41460  dochkr1OLDN  41461  hdmap1fval  41778  lcmineqlem13  42022  unitscyglem4  42179  fiabv  42522  selvcllem5  42568  mhpind  42580  pellexlem5  42820  rmyabs  42946  jm2.24  42951  islssfgi  43060  pwslnm  43082  dgraaub  43136  omlimcl2  43230  onexoegt  43232  rp-oelim2  43297  oeord2lim  43298  oeord2i  43299  ensucne0OLD  43519  iscard5  43525  clrellem  43611  frege114d  43747  frege55lem1a  43855  frege70  43922  gneispace  44123  ismnushort  44296  3impexpbicom  44476  ee3bir  44500  vk15.4j  44525  onfrALTlem2  44543  ax6e2nd  44555  dfvd1impr  44573  dfvd2impr  44601  e1bir  44627  e2bir  44630  e3bir  44736  suctrALT  44823  19.21a3con13vVD  44849  3impexpbicomVD  44854  tratrbVD  44858  ssralv2VD  44863  truniALTVD  44875  trintALTVD  44877  undif3VD  44879  csbingVD  44881  onfrALTlem3VD  44884  onfrALTlem2VD  44886  onfrALTVD  44888  csbsngVD  44890  csbxpgVD  44891  csbrngVD  44893  csbunigVD  44895  csbfv12gALTVD  44896  relopabVD  44898  ax6e2ndVD  44905  2uasbanhVD  44908  vk15.4jVD  44911  sspwimp  44915  sspwimpVD  44916  sspwimpcf  44917  sspwimpcfVD  44918  suctrALTcf  44919  suctrALTcfVD  44920  suctrALT3  44921  sspwimpALT  44922  unisnALT  44923  ax6e2ndALT  44927  isosctrlem1ALT  44931  iunconnlem2  44932  prclaxpr  44947  wfaxrep  44949  supminfxrrnmpt  45420  limsuppnflem  45665  limsupubuz  45668  cncfuni  45841  iblcncfioo  45933  stoweidlem14  45969  stoweidlem17  45972  stoweidlem35  45990  stoweidlem57  46012  stirlinglem7  46035  stirlinglem10  46038  fourierdlem54  46115  fourierdlem62  46123  fourierdlem63  46124  fourierdlem65  46126  fourierdlem73  46134  fourierdlem80  46141  fourierdlem82  46143  fourierdlem101  46162  etransclem32  46221  ioorrnopnxr  46262  subsaliuncl  46313  meadjiunlem  46420  ismeannd  46422  voliunsge0lem  46427  volmea  46429  caratheodory  46483  ovnsubaddlem2  46526  hoidmvlelem5  46554  hoiqssbllem2  46578  iinhoiicc  46629  aibandbiaiaiffb  46844  funressnvmo  46994  dfdfat2  47077  afvres  47121  tz6.12-afv  47122  ndmaovass  47155  afv2res  47188  tz6.12-afv2  47189  el1fzopredsuc  47274  zp1modne  47285  fundcmpsurinjimaid  47335  iccpartiltu  47346  iccelpart  47357  lswn0  47368  ichnfimlem  47387  prprelb  47440  evenprm2  47638  dfnbgr6  47780  dfsclnbgr6  47781  isgrtri  47847  lincext1  48299  sepfsepc  48723  isclatd  48771  intubeu  48772  unilbeu  48773  fullthinc  48845  setc2othin  48856