Theorem biimpri 227

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mpbir  230  sylibr  233  sylbir  234  sylbbr  235  sylbb1  236  sylbb2  237  syl5bir  242  syl6ibr  251  mtbi  322  sylnib  328  simplbi2  501  sylanbr  582  sylan2br  595  pm2.54  849  orbi2i  910  pm2.31  920  pm2.85  930  pm3.11  990  syl3an1br  1405  syl3an2br  1406  syl3an3br  1407  had1  1605  nic-axALT  1677  speimfw  1968  sbbii  2080  hbsbw  2170  mobii  2549  mo4  2567  nfabdwOLD  2932  r19.30  3269  r19.30OLD  3270  ceqsexv2d  3482  eueq2  3646  ralun  4127  ssunieq  4877  ax6vsep  5228  opelxpi  5627  ordunidif  6318  unizlim  6387  dffo2  6701  dff1o2  6730  resdif  6746  f1o00  6760  fvimacnvALT  6943  fvcofneq  6978  exfo  6990  ressnop0  7034  fsnunfv  7068  ovid  7423  ovidig  7424  dfwe2  7633  onminex  7661  nnsuc  7739  1stnpr  7844  2ndnpr  7845  f1stres  7864  f2ndres  7865  1st2val  7868  2nd2val  7869  frxp  7976  soxp  7979  fprlem1  8125  tz7.49  8285  elixpsn  8734  domdifsn  8850  domunsncan  8868  unfi  8964  cnvfi  8972  fineqvlem  9046  unblem4  9078  ordiso2  9283  zfreg  9363  inf3lem3  9397  trcl  9495  unir1  9580  ssrankr1  9602  djuunxp  9688  pm54.43lem  9767  infxpenlem  9778  ween  9800  acni3  9812  kmlem1  9915  infdif  9974  ackbij1lem1  9985  fin23lem32  10109  isfin1-3  10151  axdc3lem2  10216  ac6c4  10246  zornn0g  10270  axdclem2  10285  rnct  10290  brdom3  10293  brdom5  10294  brdom4  10295  brdom6disj  10297  konigthlem  10333  pwcfsdom  10348  cfpwsdom  10349  alephom  10350  gruina  10583  grur1  10585  grothomex  10594  grothac  10595  nqpr  10779  axcnre  10929  axpre-sup  10934  ssxr  11053  le2tri3i  11114  muldivdir  11677  0nn0  12257  uzind4  12655  rpnnen1lem5  12730  elfz4  13258  eluzfz  13260  ssfzo12bi  13491  hashgt0elex  14125  hashgt23el  14148  hashxplem  14157  hashfun  14161  ishashinf  14186  wrdsymb1  14265  ccatfv0  14297  lswccats1fst  14354  ccatswrd  14390  ccatpfx  14423  splfv1  14477  repswfsts  14503  cshinj  14533  swrdco  14559  cotr2g  14696  trclun  14734  resqrex  14971  sumeven  16105  ndvdsadd  16128  gcdcllem1  16215  gcdcllem3  16217  lcmftp  16350  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  lcmfun  16359  coprmprod  16375  coprmproddvdslem  16376  divgcdcoprmex  16380  1idssfct  16394  prmodvdslcmf  16757  cshwrepswhash1  16813  xpsfrnel2  17284  xpsff1o  17287  catcone0  17405  initoeu2  17740  clatlem  18229  clatlubcl2  18231  clatglbcl2  18233  xpsmnd  18434  xpsgrp  18703  mulgfval  18711  gsmsymgrfix  19045  pmtr3ncom  19092  gsumcom3fi  19589  dprdfeq0  19634  gsumdixp  19857  lspcl  20247  lindfind  21032  lindsind  21033  lindsind2  21035  lindff1  21036  f1linds  21041  mat1dimscm  21633  mdetunilem7  21776  fvmptnn04if  22007  tgcl  22128  elcls  22233  opnnei  22280  neiptopnei  22292  cnpnei  22424  cmpfii  22569  txcnp  22780  xpstps  22970  fbun  23000  isfild  23018  snfil  23024  filconn  23043  isufil2  23068  hauspwpwf1  23147  cnextcn  23227  ustfilxp  23373  ustuqtop4  23405  xpsxms  23699  xpsms  23700  rlmnvc  23876  nmoid  23915  xrsmopn  23984  xrhmeo  24118  cphsqrtcl  24357  iscmet3  24466  iundisj  24721  ioorinv  24749  bddiblnc  25015  dvtaylp  25538  logbid1  25927  logbchbase  25930  relogbcxpb  25946  logbmpt  25947  logbfval  25949  musum  26349  lgsmodeq  26499  lgsmulsqcoprm  26500  2lgs  26564  2sqnn0  26595  pntlem3  26766  nbupgrel  27721  nbusgrvtxm1  27755  nb3gr2nb  27760  pthdivtx  28106  pthdlem2lem  28144  crctisclwlk  28171  wwlks  28209  wwlksonvtx  28229  wspthnonp  28233  wlkiswwlks2lem1  28243  wwlksnndef  28279  wwlksnfi  28280  clwlkclwwlkf1lem3  28379  clwlkclwwlkf1  28383  clwwlknnn  28406  clwwlkel  28419  clwwlkf1  28422  wwlksext2clwwlk  28430  clwwlknonwwlknonb  28479  umgr3v3e3cycl  28557  frgrncvvdeq  28682  sspval  29094  blo3i  29173  ajfval  29180  spanval  29704  cmcmlem  29962  leopnmid  30509  csmdsymi  30705  chirredlem4  30764  sumdmdlem  30789  iundisjf  30937  padct  31063  iundisjfi  31126  hashxpe  31136  fprodex01  31148  xrpxdivcld  31218  lsmsnorb  31588  mxidlnzr  31648  extdgval  31738  ccfldextdgrr  31751  pnfneige0  31910  rrhre  31980  esumcocn  32057  hasheuni  32062  sgon  32101  sigapildsys  32139  ddemeas  32213  dya2iocct  32256  dya2iocnrect  32257  eulerpartgbij  32348  eulerpartlemgs2  32356  coinflippv  32459  signstfvneq0  32560  hgt750lemb  32645  bnj1136  32986  bnj1175  32993  bnj1408  33025  fnrelpredd  33070  pthhashvtx  33098  spthcycl  33100  upgracycumgr  33124  umgracycusgr  33125  cvmsdisj  33241  mrsubvrs  33493  mppspstlem  33542  problem4  33635  climuzcnv  33638  dford5  33680  dfon2lem7  33774  frxp2  33800  sltval2  33868  noxp1o  33875  conway  34002  scutbdaylt  34021  imageval  34241  filnetlem2  34577  df3nandALT1  34597  lukshef-ax2  34613  arg-ax  34614  bj-andnotim  34779  bj-modalbe  34879  bj-hbs1  35003  bj-hbsb2av  35005  bj-2uplex  35221  mptsnunlem  35518  onsucuni3  35547  fvineqsneq  35592  finixpnum  35771  fin2solem  35772  matunitlindflem2  35783  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem32  35818  mblfinlem3  35825  itg2addnclem2  35838  itg2addnc  35840  ftc1anclem6  35864  heiborlem3  35980  ismndo2  36041  rngomndo  36102  isfld2  36172  isfldidl  36235  dmncan2  36244  oprabbi  36328  opabbi  36332  ac6s3f  36338  relcnveq3  36463  elrelscnveq3  36616  lsat0cv  37054  pclfinclN  37971  docavalN  39144  djavalN  39156  dochval  39372  djhval  39419  dochexmidlem8  39488  dochkr1  39499  dochkr1OLDN  39500  hdmap1fval  39817  lcmineqlem13  40056  selvval2lem5  40236  mhpind  40290  pellexlem5  40662  rmyabs  40787  jm2.24  40792  islssfgi  40904  pwslnm  40926  dgraaub  40980  ensucne0OLD  41144  iscard5  41150  clrellem  41237  frege114d  41373  frege55lem1a  41481  frege70  41548  gneispace  41751  ismnushort  41926  3impexpbicom  42106  ee3bir  42130  vk15.4j  42155  onfrALTlem2  42173  ax6e2nd  42185  dfvd1impr  42203  dfvd2impr  42231  e1bir  42257  e2bir  42260  e3bir  42366  suctrALT  42453  19.21a3con13vVD  42479  3impexpbicomVD  42484  tratrbVD  42488  ssralv2VD  42493  truniALTVD  42505  trintALTVD  42507  undif3VD  42509  onfrALTlem3VD  42514  onfrALTlem2VD  42516  onfrALTVD  42518  relopabVD  42528  ax6e2ndVD  42535  2uasbanhVD  42538  vk15.4jVD  42541  sspwimp  42545  sspwimpVD  42546  sspwimpcf  42547  sspwimpcfVD  42548  suctrALTcf  42549  suctrALTcfVD  42550  suctrALT3  42551  sspwimpALT  42552  unisnALT  42553  ax6e2ndALT  42557  isosctrlem1ALT  42561  iunconnlem2  42562  supminfxrrnmpt  43018  limsuppnflem  43258  limsupubuz  43261  cncfuni  43434  iblcncfioo  43526  stoweidlem14  43562  stoweidlem17  43565  stoweidlem35  43583  stoweidlem57  43605  stirlinglem7  43628  stirlinglem10  43631  fourierdlem54  43708  fourierdlem62  43716  fourierdlem63  43717  fourierdlem65  43719  fourierdlem73  43727  fourierdlem80  43734  fourierdlem82  43736  fourierdlem101  43755  etransclem32  43814  ioorrnopnxr  43855  subsaliuncl  43904  meadjiunlem  44010  ismeannd  44012  voliunsge0lem  44017  volmea  44019  caratheodory  44073  ovnsubaddlem2  44116  hoidmvlelem5  44144  hoiqssbllem2  44168  iinhoiicc  44219  aibandbiaiaiffb  44401  funressnvmo  44550  dfdfat2  44631  afvres  44675  tz6.12-afv  44676  ndmaovass  44709  afv2res  44742  tz6.12-afv2  44743  el1fzopredsuc  44828  fzoopth  44830  fundcmpsurinjimaid  44874  iccpartiltu  44885  iccelpart  44896  lswn0  44907  ichnfimlem  44926  prprelb  44979  evenprm2  45177  lincext1  45806  sepfsepc  46232  isclatd  46280  intubeu  46281  unilbeu  46282  fullthinc  46338  setc2othin  46348