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  1407  syl3an2br  1408  syl3an3br  1409  had1  1602  nic-axALT  1673  speimfw  1962  sbbii  2075  hbsbwOLD  2171  mobii  2546  mo4  2564  r19.30  3107  r19.30OLD  3108  ceqsexv2dOLD  3517  eueq2  3698  ralun  4178  ssunieq  4923  ax6vsep  5283  opelxpi  5702  ordunidif  6413  unizlim  6487  dffo2  6804  dff1o2  6833  resdif  6849  f1o00  6863  fvimacnvALT  7057  fvcofneq  7093  exfo  7105  ressnop0  7153  fsnunfv  7189  ovid  7556  ovidig  7557  dfwe2  7776  dford5  7786  onminex  7804  nnsuc  7887  1stnpr  8000  2ndnpr  8001  f1stres  8020  f2ndres  8021  1st2val  8024  2nd2val  8025  frxp  8133  soxp  8136  frxp2  8151  fprlem1  8307  tz7.49  8467  elixpsn  8959  domdifsn  9076  domunsncan  9094  unfi  9193  cnvfi  9198  fineqvlem  9280  unblem4  9313  ordiso2  9537  zfreg  9617  inf3lem3  9652  trcl  9750  unir1  9835  ssrankr1  9857  djuunxp  9943  pm54.43lem  10022  infxpenlem  10035  ween  10057  acni3  10069  kmlem1  10173  infdif  10230  ackbij1lem1  10241  fin23lem32  10366  isfin1-3  10408  axdc3lem2  10473  ac6c4  10503  zornn0g  10527  axdclem2  10542  rnct  10547  brdom3  10550  brdom5  10551  brdom4  10552  brdom6disj  10554  konigthlem  10590  pwcfsdom  10605  cfpwsdom  10606  alephom  10607  gruina  10840  grur1  10842  grothomex  10851  grothac  10852  nqpr  11036  axcnre  11186  axpre-sup  11191  ssxr  11312  le2tri3i  11373  muldivdir  11942  0nn0  12524  uzind4  12930  rpnnen1lem5  13005  elfz4  13539  eluzfz  13541  ssfzo12bi  13782  fzoopth  13783  hashgt0elex  14423  hashgt23el  14446  hashxplem  14455  hashfun  14459  ishashinf  14485  wrdsymb1  14574  ccatfv0  14604  lswccats1fst  14656  ccatswrd  14689  ccatpfx  14722  splfv1  14776  repswfsts  14802  cshinj  14832  swrdco  14859  cotr2g  14998  trclun  15036  resqrex  15272  sumeven  16407  ndvdsadd  16430  gcdcllem1  16519  gcdcllem3  16521  lcmftp  16656  lcmfunsnlem2lem2  16659  lcmfunsnlem2  16660  lcmfun  16665  coprmprod  16681  coprmproddvdslem  16682  divgcdcoprmex  16686  1idssfct  16700  prmodvdslcmf  17068  cshwrepswhash1  17123  xpsfrnel2  17581  xpsff1o  17584  catcone0  17702  initoeu2  18033  clatlem  18517  clatlubcl2  18519  clatglbcl2  18521  xpsmnd  18760  xpsgrp  19047  mulgfval  19057  gsmsymgrfix  19415  pmtr3ncom  19462  gsumcom3fi  19966  dprdfeq0  20011  gsumdixp  20285  lspcl  20943  lindfind  21791  lindsind  21792  lindsind2  21794  lindff1  21795  f1linds  21800  evls1maplmhm  22330  mat1dimscm  22430  mdetunilem7  22573  fvmptnn04if  22804  tgcl  22924  elcls  23028  opnnei  23075  neiptopnei  23087  cnpnei  23219  cmpfii  23364  txcnp  23575  xpstps  23765  fbun  23795  isfild  23813  snfil  23819  filconn  23838  isufil2  23863  hauspwpwf1  23942  cnextcn  24022  ustfilxp  24168  ustuqtop4  24200  xpsxms  24492  xpsms  24493  rlmnvc  24661  nmoid  24700  xrsmopn  24771  xrhmeo  24914  cphsqrtcl  25155  iscmet3  25264  iundisj  25520  ioorinv  25548  bddiblnc  25814  dvtaylp  26349  logbid1  26748  logbchbase  26751  relogbcxpb  26767  logbmpt  26768  logbfval  26770  musum  27171  lgsmodeq  27323  lgsmulsqcoprm  27324  2lgs  27388  2sqnn0  27419  pntlem3  27590  sltval2  27638  noxp1o  27645  conway  27781  scutbdaylt  27800  nbupgrel  29291  nbusgrvtxm1  29325  nb3gr2nb  29330  pthdivtx  29676  pthdlem2lem  29716  crctisclwlk  29743  wwlks  29784  wwlksonvtx  29804  wspthnonp  29808  wlkiswwlks2lem1  29818  wwlksnndef  29854  wwlksnfi  29855  clwlkclwwlkf1lem3  29954  clwlkclwwlkf1  29958  clwwlknnn  29981  clwwlkel  29994  clwwlkf1  29997  wwlksext2clwwlk  30005  clwwlknonwwlknonb  30054  umgr3v3e3cycl  30132  frgrncvvdeq  30257  sspval  30671  blo3i  30750  ajfval  30757  spanval  31281  cmcmlem  31539  leopnmid  32086  csmdsymi  32282  chirredlem4  32341  sumdmdlem  32366  iundisjf  32538  padct  32667  iundisjfi  32742  nn0difffzod  32752  hashxpe  32755  fprodex01  32772  xrpxdivcld  32862  gsumfs2d  33002  fldgensdrg  33261  lsmsnorb  33359  mxidlnzr  33435  zringfrac  33522  lactlmhm  33625  extdgval  33646  ccfldextdgrr  33664  ply1annprmidl  33692  pnfneige0  33925  rrhre  33997  esumcocn  34056  hasheuni  34061  sgon  34100  sigapildsys  34138  ddemeas  34212  dya2iocct  34257  dya2iocnrect  34258  eulerpartgbij  34349  eulerpartlemgs2  34357  coinflippv  34461  signstfvneq0  34562  hgt750lemb  34646  bnj1136  34986  bnj1175  34993  bnj1408  35025  fnrelpredd  35078  pthhashvtx  35108  spthcycl  35109  upgracycumgr  35133  umgracycusgr  35134  cvmsdisj  35250  mrsubvrs  35502  mppspstlem  35551  problem4  35648  climuzcnv  35651  currybi  35668  dfon2lem7  35765  imageval  35906  filnetlem2  36355  df3nandALT1  36375  lukshef-ax2  36391  arg-ax  36392  weiunpo  36441  bj-andnotim  36564  bj-modalbe  36664  bj-hbs1  36788  bj-hbsb2av  36790  bj-2uplex  36998  mptsnunlem  37314  onsucuni3  37343  fvineqsneq  37388  finixpnum  37587  fin2solem  37588  matunitlindflem2  37599  poimirlem6  37608  poimirlem7  37609  poimirlem8  37610  poimirlem18  37620  poimirlem21  37623  poimirlem22  37624  poimirlem32  37634  mblfinlem3  37641  itg2addnclem2  37654  itg2addnc  37656  ftc1anclem6  37680  heiborlem3  37795  ismndo2  37856  rngomndo  37917  isfld2  37987  isfldidl  38050  dmncan2  38059  oprabbi  38143  opabbi  38147  ac6s3f  38153  relcnveq3  38297  elrelscnveq3  38467  lsat0cv  39009  pclfinclN  39927  docavalN  41100  djavalN  41112  dochval  41328  djhval  41375  dochexmidlem8  41444  dochkr1  41455  dochkr1OLDN  41456  hdmap1fval  41773  lcmineqlem13  42017  unitscyglem4  42174  fiabv  42525  selvcllem5  42571  mhpind  42583  pellexlem5  42822  rmyabs  42948  jm2.24  42953  islssfgi  43062  pwslnm  43084  dgraaub  43138  omlimcl2  43232  onexoegt  43234  rp-oelim2  43298  oeord2lim  43299  oeord2i  43300  ensucne0OLD  43520  iscard5  43526  clrellem  43612  frege114d  43748  frege55lem1a  43856  frege70  43923  gneispace  44124  ismnushort  44292  3impexpbicom  44472  ee3bir  44495  vk15.4j  44520  onfrALTlem2  44538  ax6e2nd  44550  dfvd1impr  44568  dfvd2impr  44596  e1bir  44622  e2bir  44625  e3bir  44731  suctrALT  44818  19.21a3con13vVD  44844  3impexpbicomVD  44849  tratrbVD  44853  ssralv2VD  44858  truniALTVD  44870  trintALTVD  44872  undif3VD  44874  csbingVD  44876  onfrALTlem3VD  44879  onfrALTlem2VD  44881  onfrALTVD  44883  csbsngVD  44885  csbxpgVD  44886  csbrngVD  44888  csbunigVD  44890  csbfv12gALTVD  44891  relopabVD  44893  ax6e2ndVD  44900  2uasbanhVD  44903  vk15.4jVD  44906  sspwimp  44910  sspwimpVD  44911  sspwimpcf  44912  sspwimpcfVD  44913  suctrALTcf  44914  suctrALTcfVD  44915  suctrALT3  44916  sspwimpALT  44917  unisnALT  44918  ax6e2ndALT  44922  isosctrlem1ALT  44926  iunconnlem2  44927  prclaxpr  44974  wfaxrep  44983  supminfxrrnmpt  45454  limsuppnflem  45697  limsupubuz  45700  cncfuni  45873  iblcncfioo  45965  stoweidlem14  46001  stoweidlem17  46004  stoweidlem35  46022  stoweidlem57  46044  stirlinglem7  46067  stirlinglem10  46070  fourierdlem54  46147  fourierdlem62  46155  fourierdlem63  46156  fourierdlem65  46158  fourierdlem73  46166  fourierdlem80  46173  fourierdlem82  46175  fourierdlem101  46194  etransclem32  46253  ioorrnopnxr  46294  subsaliuncl  46345  meadjiunlem  46452  ismeannd  46454  voliunsge0lem  46459  volmea  46461  caratheodory  46515  ovnsubaddlem2  46558  hoidmvlelem5  46586  hoiqssbllem2  46610  iinhoiicc  46661  aibandbiaiaiffb  46880  funressnvmo  47030  dfdfat2  47113  afvres  47157  tz6.12-afv  47158  ndmaovass  47191  afv2res  47224  tz6.12-afv2  47225  el1fzopredsuc  47310  zp1modne  47321  fundcmpsurinjimaid  47371  iccpartiltu  47382  iccelpart  47393  lswn0  47404  ichnfimlem  47423  prprelb  47476  evenprm2  47674  dfnbgr6  47816  dfsclnbgr6  47817  isgrtri  47883  lincext1  48344  resinsnALT  48756  tposideq  48771  sepfsepc  48809  isclatd  48864  intubeu  48865  unilbeu  48866  uprcl2  48972  functhincfun  49150  fullthinc  49151  setc2othin  49165