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  2076  hbsbwOLD  2172  mobii  2547  mo4  2565  r19.30  3107  ceqsexv2dOLD  3513  eueq2  3693  ralun  4173  ssunieq  4919  ax6vsep  5273  opelxpi  5691  ordunidif  6402  unizlim  6476  dffo2  6793  dff1o2  6822  resdif  6838  f1o00  6852  fvimacnvALT  7046  fvcofneq  7082  exfo  7094  ressnop0  7142  fsnunfv  7178  2f1fvneq  7252  ovid  7546  ovidig  7547  dfwe2  7766  dford5  7776  onminex  7794  nnsuc  7877  1stnpr  7990  2ndnpr  7991  f1stres  8010  f2ndres  8011  1st2val  8014  2nd2val  8015  frxp  8123  soxp  8126  frxp2  8141  fprlem1  8297  tz7.49  8457  elixpsn  8949  domdifsn  9066  domunsncan  9084  unfi  9183  cnvfi  9188  fineqvlem  9268  unblem4  9301  ordiso2  9527  zfreg  9607  inf3lem3  9642  trcl  9740  unir1  9825  ssrankr1  9847  djuunxp  9933  pm54.43lem  10012  infxpenlem  10025  ween  10047  acni3  10059  kmlem1  10163  infdif  10220  ackbij1lem1  10231  fin23lem32  10356  isfin1-3  10398  axdc3lem2  10463  ac6c4  10493  zornn0g  10517  axdclem2  10532  rnct  10537  brdom3  10540  brdom5  10541  brdom4  10542  brdom6disj  10544  konigthlem  10580  pwcfsdom  10595  cfpwsdom  10596  alephom  10597  gruina  10830  grur1  10832  grothomex  10841  grothac  10842  nqpr  11026  axcnre  11176  axpre-sup  11181  ssxr  11302  le2tri3i  11363  muldivdir  11932  0nn0  12514  uzind4  12920  rpnnen1lem5  12995  elfz4  13532  eluzfz  13534  ssfzo12bi  13775  fzoopth  13776  hashgt0elex  14417  hashgt23el  14440  hashxplem  14449  hashfun  14453  ishashinf  14479  wrdsymb1  14569  ccatfv0  14599  lswccats1fst  14651  ccatswrd  14684  ccatpfx  14717  splfv1  14771  repswfsts  14797  cshinj  14827  swrdco  14854  cotr2g  14993  trclun  15031  resqrex  15267  sumeven  16404  ndvdsadd  16427  gcdcllem1  16516  gcdcllem3  16518  lcmftp  16653  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  lcmfun  16662  coprmprod  16678  coprmproddvdslem  16679  divgcdcoprmex  16683  1idssfct  16697  prmodvdslcmf  17065  cshwrepswhash1  17120  xpsfrnel2  17576  xpsff1o  17579  catcone0  17697  initoeu2  18027  clatlem  18510  clatlubcl2  18512  clatglbcl2  18514  xpsmnd  18753  xpsgrp  19040  mulgfval  19050  gsmsymgrfix  19407  pmtr3ncom  19454  gsumcom3fi  19958  dprdfeq0  20003  gsumdixp  20277  lspcl  20931  lindfind  21774  lindsind  21775  lindsind2  21777  lindff1  21778  f1linds  21783  evls1maplmhm  22313  mat1dimscm  22411  mdetunilem7  22554  fvmptnn04if  22785  tgcl  22905  elcls  23009  opnnei  23056  neiptopnei  23068  cnpnei  23200  cmpfii  23345  txcnp  23556  xpstps  23746  fbun  23776  isfild  23794  snfil  23800  filconn  23819  isufil2  23844  hauspwpwf1  23923  cnextcn  24003  ustfilxp  24149  ustuqtop4  24181  xpsxms  24471  xpsms  24472  rlmnvc  24640  nmoid  24679  xrsmopn  24750  xrhmeo  24893  cphsqrtcl  25134  iscmet3  25243  iundisj  25499  ioorinv  25527  bddiblnc  25793  dvtaylp  26328  logbid1  26728  logbchbase  26731  relogbcxpb  26747  logbmpt  26748  logbfval  26750  musum  27151  lgsmodeq  27303  lgsmulsqcoprm  27304  2lgs  27368  2sqnn0  27399  pntlem3  27570  sltval2  27618  noxp1o  27625  conway  27761  scutbdaylt  27780  nbupgrel  29270  nbusgrvtxm1  29304  nb3gr2nb  29309  pthdivtx  29655  pthdlem2lem  29695  crctisclwlk  29722  wwlks  29763  wwlksonvtx  29783  wspthnonp  29787  wlkiswwlks2lem1  29797  wwlksnndef  29833  wwlksnfi  29834  clwlkclwwlkf1lem3  29933  clwlkclwwlkf1  29937  clwwlknnn  29960  clwwlkel  29973  clwwlkf1  29976  wwlksext2clwwlk  29984  clwwlknonwwlknonb  30033  umgr3v3e3cycl  30111  frgrncvvdeq  30236  sspval  30650  blo3i  30729  ajfval  30736  spanval  31260  cmcmlem  31518  leopnmid  32065  csmdsymi  32261  chirredlem4  32320  sumdmdlem  32345  iundisjf  32516  padct  32643  iundisjfi  32719  nn0difffzod  32729  hashxpe  32732  fprodex01  32750  xrpxdivcld  32855  gsumfs2d  32995  fldgensdrg  33254  lsmsnorb  33352  mxidlnzr  33428  zringfrac  33515  lactlmhm  33620  extdgval  33641  ccfldextdgrr  33659  ply1annprmidl  33687  pnfneige0  33928  rrhre  33998  esumcocn  34057  hasheuni  34062  sgon  34101  sigapildsys  34139  ddemeas  34213  dya2iocct  34258  dya2iocnrect  34259  eulerpartgbij  34350  eulerpartlemgs2  34358  coinflippv  34462  signstfvneq0  34550  hgt750lemb  34634  bnj1136  34974  bnj1175  34981  bnj1408  35013  fnrelpredd  35066  pthhashvtx  35096  spthcycl  35097  upgracycumgr  35121  umgracycusgr  35122  cvmsdisj  35238  mrsubvrs  35490  mppspstlem  35539  problem4  35636  climuzcnv  35639  currybi  35656  dfon2lem7  35753  imageval  35894  filnetlem2  36343  df3nandALT1  36363  lukshef-ax2  36379  arg-ax  36380  weiunpo  36429  bj-andnotim  36552  bj-modalbe  36652  bj-hbs1  36776  bj-hbsb2av  36778  bj-2uplex  36986  mptsnunlem  37302  onsucuni3  37331  fvineqsneq  37376  finixpnum  37575  fin2solem  37576  matunitlindflem2  37587  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem32  37622  mblfinlem3  37629  itg2addnclem2  37642  itg2addnc  37644  ftc1anclem6  37668  heiborlem3  37783  ismndo2  37844  rngomndo  37905  isfld2  37975  isfldidl  38038  dmncan2  38047  oprabbi  38131  opabbi  38135  ac6s3f  38141  relcnveq3  38285  elrelscnveq3  38455  lsat0cv  38997  pclfinclN  39915  docavalN  41088  djavalN  41100  dochval  41316  djhval  41363  dochexmidlem8  41432  dochkr1  41443  dochkr1OLDN  41444  hdmap1fval  41761  lcmineqlem13  42000  unitscyglem4  42157  fiabv  42506  selvcllem5  42552  mhpind  42564  pellexlem5  42803  rmyabs  42929  jm2.24  42934  islssfgi  43043  pwslnm  43065  dgraaub  43119  omlimcl2  43213  onexoegt  43215  rp-oelim2  43279  oeord2lim  43280  oeord2i  43281  ensucne0OLD  43501  iscard5  43507  clrellem  43593  frege114d  43729  frege55lem1a  43837  frege70  43904  gneispace  44105  ismnushort  44273  3impexpbicom  44453  ee3bir  44476  vk15.4j  44501  onfrALTlem2  44519  ax6e2nd  44531  dfvd1impr  44549  dfvd2impr  44577  e1bir  44603  e2bir  44606  e3bir  44711  suctrALT  44798  19.21a3con13vVD  44824  3impexpbicomVD  44829  tratrbVD  44833  ssralv2VD  44838  truniALTVD  44850  trintALTVD  44852  undif3VD  44854  csbingVD  44856  onfrALTlem3VD  44859  onfrALTlem2VD  44861  onfrALTVD  44863  csbsngVD  44865  csbxpgVD  44866  csbrngVD  44868  csbunigVD  44870  csbfv12gALTVD  44871  relopabVD  44873  ax6e2ndVD  44880  2uasbanhVD  44883  vk15.4jVD  44886  sspwimp  44890  sspwimpVD  44891  sspwimpcf  44892  sspwimpcfVD  44893  suctrALTcf  44894  suctrALTcfVD  44895  suctrALT3  44896  sspwimpALT  44897  unisnALT  44898  ax6e2ndALT  44902  isosctrlem1ALT  44906  iunconnlem2  44907  prclaxpr  44958  wfaxrep  44967  supminfxrrnmpt  45446  limsuppnflem  45687  limsupubuz  45690  cncfuni  45863  iblcncfioo  45955  stoweidlem14  45991  stoweidlem17  45994  stoweidlem35  46012  stoweidlem57  46034  stirlinglem7  46057  stirlinglem10  46060  fourierdlem54  46137  fourierdlem62  46145  fourierdlem63  46146  fourierdlem65  46148  fourierdlem73  46156  fourierdlem80  46163  fourierdlem82  46165  fourierdlem101  46184  etransclem32  46243  ioorrnopnxr  46284  subsaliuncl  46335  meadjiunlem  46442  ismeannd  46444  voliunsge0lem  46449  volmea  46451  caratheodory  46505  ovnsubaddlem2  46548  hoidmvlelem5  46576  hoiqssbllem2  46600  iinhoiicc  46651  aibandbiaiaiffb  46872  funressnvmo  47022  dfdfat2  47105  afvres  47149  tz6.12-afv  47150  ndmaovass  47183  afv2res  47216  tz6.12-afv2  47217  el1fzopredsuc  47302  zp1modne  47323  fundcmpsurinjimaid  47373  iccpartiltu  47384  iccelpart  47395  lswn0  47406  ichnfimlem  47425  prprelb  47478  evenprm2  47676  dfnbgr6  47818  dfsclnbgr6  47819  isgrtri  47903  lincext1  48378  resinsnALT  48796  tposideq  48811  sepfsepc  48850  isclatd  48905  intubeu  48906  unilbeu  48907  uprcl2  49071  functhincfun  49283  fullthinc  49284  setc2othin  49300