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  1408  syl3an2br  1409  syl3an3br  1410  had1  1603  nic-axALT  1674  speimfw  1963  sbbii  2077  hbsbwOLD  2173  mobii  2542  mo4  2560  r19.30  3101  ceqsexv2dOLD  3503  eueq2  3684  ralun  4164  ssunieq  4910  ax6vsep  5261  opelxpi  5678  ordunidif  6385  unizlim  6460  dffo2  6779  dff1o2  6808  resdif  6824  f1o00  6838  fvimacnvALT  7032  fvcofneq  7068  exfo  7080  ressnop0  7128  fsnunfv  7164  2f1fvneq  7238  ovid  7533  ovidig  7534  dfwe2  7753  dford5  7763  onminex  7781  nnsuc  7863  1stnpr  7975  2ndnpr  7976  f1stres  7995  f2ndres  7996  1st2val  7999  2nd2val  8000  frxp  8108  soxp  8111  frxp2  8126  fprlem1  8282  tz7.49  8416  elixpsn  8913  domdifsn  9028  domunsncan  9046  unfi  9141  cnvfi  9146  fineqvlem  9216  unblem4  9249  ordiso2  9475  zfreg  9555  inf3lem3  9590  trcl  9688  unir1  9773  ssrankr1  9795  djuunxp  9881  pm54.43lem  9960  infxpenlem  9973  ween  9995  acni3  10007  kmlem1  10111  infdif  10168  ackbij1lem1  10179  fin23lem32  10304  isfin1-3  10346  axdc3lem2  10411  ac6c4  10441  zornn0g  10465  axdclem2  10480  rnct  10485  brdom3  10488  brdom5  10489  brdom4  10490  brdom6disj  10492  konigthlem  10528  pwcfsdom  10543  cfpwsdom  10544  alephom  10545  gruina  10778  grur1  10780  grothomex  10789  grothac  10790  nqpr  10974  axcnre  11124  axpre-sup  11129  ssxr  11250  le2tri3i  11311  muldivdir  11882  0nn0  12464  uzind4  12872  rpnnen1lem5  12947  elfz4  13485  eluzfz  13487  ssfzo12bi  13729  fzoopth  13730  hashgt0elex  14373  hashgt23el  14396  hashxplem  14405  hashfun  14409  ishashinf  14435  wrdsymb1  14525  ccatfv0  14555  lswccats1fst  14607  ccatswrd  14640  ccatpfx  14673  splfv1  14727  repswfsts  14753  cshinj  14783  swrdco  14810  cotr2g  14949  trclun  14987  resqrex  15223  sumeven  16364  ndvdsadd  16387  gcdcllem1  16476  gcdcllem3  16478  lcmftp  16613  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  lcmfun  16622  coprmprod  16638  coprmproddvdslem  16639  divgcdcoprmex  16643  1idssfct  16657  prmodvdslcmf  17025  cshwrepswhash1  17080  xpsfrnel2  17534  xpsff1o  17537  catcone0  17655  initoeu2  17985  clatlem  18468  clatlubcl2  18470  clatglbcl2  18472  xpsmnd  18711  xpsgrp  18998  mulgfval  19008  gsmsymgrfix  19365  pmtr3ncom  19412  gsumcom3fi  19916  dprdfeq0  19961  gsumdixp  20235  lspcl  20889  lindfind  21732  lindsind  21733  lindsind2  21735  lindff1  21736  f1linds  21741  evls1maplmhm  22271  mat1dimscm  22369  mdetunilem7  22512  fvmptnn04if  22743  tgcl  22863  elcls  22967  opnnei  23014  neiptopnei  23026  cnpnei  23158  cmpfii  23303  txcnp  23514  xpstps  23704  fbun  23734  isfild  23752  snfil  23758  filconn  23777  isufil2  23802  hauspwpwf1  23881  cnextcn  23961  ustfilxp  24107  ustuqtop4  24139  xpsxms  24429  xpsms  24430  rlmnvc  24598  nmoid  24637  xrsmopn  24708  xrhmeo  24851  cphsqrtcl  25091  iscmet3  25200  iundisj  25456  ioorinv  25484  bddiblnc  25750  dvtaylp  26285  logbid1  26685  logbchbase  26688  relogbcxpb  26704  logbmpt  26705  logbfval  26707  musum  27108  lgsmodeq  27260  lgsmulsqcoprm  27261  2lgs  27325  2sqnn0  27356  pntlem3  27527  sltval2  27575  noxp1o  27582  conway  27718  scutbdaylt  27737  nbupgrel  29279  nbusgrvtxm1  29313  nb3gr2nb  29318  pthdivtx  29664  pthdlem2lem  29704  crctisclwlk  29731  wwlks  29772  wwlksonvtx  29792  wspthnonp  29796  wlkiswwlks2lem1  29806  wwlksnndef  29842  wwlksnfi  29843  clwlkclwwlkf1lem3  29942  clwlkclwwlkf1  29946  clwwlknnn  29969  clwwlkel  29982  clwwlkf1  29985  wwlksext2clwwlk  29993  clwwlknonwwlknonb  30042  umgr3v3e3cycl  30120  frgrncvvdeq  30245  sspval  30659  blo3i  30738  ajfval  30745  spanval  31269  cmcmlem  31527  leopnmid  32074  csmdsymi  32270  chirredlem4  32329  sumdmdlem  32354  iundisjf  32525  padct  32650  iundisjfi  32726  nn0difffzod  32736  hashxpe  32739  fprodex01  32757  xrpxdivcld  32862  gsumfs2d  33002  fldgensdrg  33271  lsmsnorb  33369  mxidlnzr  33445  zringfrac  33532  lactlmhm  33637  extdgval  33656  ccfldextdgrr  33674  ply1annprmidl  33704  pnfneige0  33948  rrhre  34018  esumcocn  34077  hasheuni  34082  sgon  34121  sigapildsys  34159  ddemeas  34233  dya2iocct  34278  dya2iocnrect  34279  eulerpartgbij  34370  eulerpartlemgs2  34378  coinflippv  34482  signstfvneq0  34570  hgt750lemb  34654  bnj1136  34994  bnj1175  35001  bnj1408  35033  fnrelpredd  35086  onvf1od  35101  vonf1owev  35102  pthhashvtx  35122  spthcycl  35123  upgracycumgr  35147  umgracycusgr  35148  cvmsdisj  35264  mrsubvrs  35516  mppspstlem  35565  problem4  35662  climuzcnv  35665  currybi  35682  dfon2lem7  35784  imageval  35925  filnetlem2  36374  df3nandALT1  36394  lukshef-ax2  36410  arg-ax  36411  weiunpo  36460  bj-andnotim  36583  bj-modalbe  36683  bj-hbs1  36807  bj-hbsb2av  36809  bj-2uplex  37017  mptsnunlem  37333  onsucuni3  37362  fvineqsneq  37407  finixpnum  37606  fin2solem  37607  matunitlindflem2  37618  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem32  37653  mblfinlem3  37660  itg2addnclem2  37673  itg2addnc  37675  ftc1anclem6  37699  heiborlem3  37814  ismndo2  37875  rngomndo  37936  isfld2  38006  isfldidl  38069  dmncan2  38078  oprabbi  38162  opabbi  38166  ac6s3f  38172  relcnveq3  38316  elrelscnveq3  38489  lsat0cv  39033  pclfinclN  39951  docavalN  41124  djavalN  41136  dochval  41352  djhval  41399  dochexmidlem8  41468  dochkr1  41479  dochkr1OLDN  41480  hdmap1fval  41797  lcmineqlem13  42036  unitscyglem4  42193  fiabv  42531  selvcllem5  42577  mhpind  42589  pellexlem5  42828  rmyabs  42954  jm2.24  42959  islssfgi  43068  pwslnm  43090  dgraaub  43144  omlimcl2  43238  onexoegt  43240  rp-oelim2  43304  oeord2lim  43305  oeord2i  43306  ensucne0OLD  43526  iscard5  43532  clrellem  43618  frege114d  43754  frege55lem1a  43862  frege70  43929  gneispace  44130  ismnushort  44297  3impexpbicom  44477  ee3bir  44500  vk15.4j  44525  onfrALTlem2  44543  ax6e2nd  44555  dfvd1impr  44573  dfvd2impr  44601  e1bir  44627  e2bir  44630  e3bir  44735  suctrALT  44822  19.21a3con13vVD  44848  3impexpbicomVD  44853  tratrbVD  44857  ssralv2VD  44862  truniALTVD  44874  trintALTVD  44876  undif3VD  44878  csbingVD  44880  onfrALTlem3VD  44883  onfrALTlem2VD  44885  onfrALTVD  44887  csbsngVD  44889  csbxpgVD  44890  csbrngVD  44892  csbunigVD  44894  csbfv12gALTVD  44895  relopabVD  44897  ax6e2ndVD  44904  2uasbanhVD  44907  vk15.4jVD  44910  sspwimp  44914  sspwimpVD  44915  sspwimpcf  44916  sspwimpcfVD  44917  suctrALTcf  44918  suctrALTcfVD  44919  suctrALT3  44920  sspwimpALT  44921  unisnALT  44922  ax6e2ndALT  44926  isosctrlem1ALT  44930  iunconnlem2  44931  prclaxpr  44982  wfaxrep  44991  supminfxrrnmpt  45474  limsuppnflem  45715  limsupubuz  45718  cncfuni  45891  iblcncfioo  45983  stoweidlem14  46019  stoweidlem17  46022  stoweidlem35  46040  stoweidlem57  46062  stirlinglem7  46085  stirlinglem10  46088  fourierdlem54  46165  fourierdlem62  46173  fourierdlem63  46174  fourierdlem65  46176  fourierdlem73  46184  fourierdlem80  46191  fourierdlem82  46193  fourierdlem101  46212  etransclem32  46271  ioorrnopnxr  46312  subsaliuncl  46363  meadjiunlem  46470  ismeannd  46472  voliunsge0lem  46477  volmea  46479  caratheodory  46533  ovnsubaddlem2  46576  hoidmvlelem5  46604  hoiqssbllem2  46628  iinhoiicc  46679  aibandbiaiaiffb  46900  funressnvmo  47050  dfdfat2  47133  afvres  47177  tz6.12-afv  47178  ndmaovass  47211  afv2res  47244  tz6.12-afv2  47245  el1fzopredsuc  47330  zp1modne  47351  fundcmpsurinjimaid  47416  iccpartiltu  47427  iccelpart  47438  lswn0  47449  ichnfimlem  47468  prprelb  47521  evenprm2  47719  dfnbgr6  47861  dfsclnbgr6  47862  isgrtri  47946  lincext1  48447  resinsnALT  48865  tposideq  48880  sepfsepc  48920  isclatd  48975  intubeu  48976  unilbeu  48977  uprcl2  49182  functhincfun  49442  fullthinc  49443  setc2othin  49459