Theorem biimpri 229

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  mpbir  232  sylibr  235  sylbir  236  sylbbr  237  sylbb1  238  sylbb2  239  biimtrrid  244  imbitrrdi  253  mtbi  323  sylnib  329  simplbi2  501  biranri  506  bilanri  507  sylanbr  588  sylan2br  601  pm2.54  858  orbi2i  918  pm2.31  928  pm2.85  938  pm3.11  1000  syl3an1br  1414  syl3an2br  1415  syl3an3br  1416  had1  1610  nic-axALT  1681  speimfw  1970  sbbii  2087  mo4  2570  r19.30  3106  ceqsexv2dOLD  3481  eueq2  3651  ralun  4127  ssunieq  4874  replem  5210  ax6vsep  5225  opelxpi  5655  ordunidif  6360  unizlim  6434  dffo2  6743  dff1o2  6772  resdif  6788  fvimacnvALT  6998  fvcofneq  7034  exfo  7046  ressnop0  7096  fsnunfv  7131  2f1fvneq  7204  ovid  7497  ovidig  7498  dfwe2  7717  dford5  7727  onminex  7745  nnsuc  7824  1stnpr  7935  2ndnpr  7936  1st2val  7959  2nd2val  7960  frxp  8066  soxp  8069  fprlem1  8240  tz7.49  8374  domdifsn  8988  domunsncan  9005  unfi  9095  cnvfi  9100  fineqvlem  9166  unblem4  9195  zfreg  9501  elirrvOLD  9503  inf3lem3  9542  unir1  9728  ssrankr1  9750  djuunxp  9836  pm54.43lem  9915  infxpenlem  9926  ween  9948  acni3  9960  kmlem1  10064  infdif  10121  ackbij1lem1  10132  fin23lem32  10257  isfin1-3  10299  axdc3lem2  10364  ac6c4  10394  zornn0g  10418  axdclem2  10433  rnct  10438  brdom3  10441  brdom5  10442  brdom4  10443  brdom6disj  10445  konigthlem  10482  pwcfsdom  10497  cfpwsdom  10498  alephom  10499  gruina  10732  grur1  10734  grothac  10744  nqpr  10928  axcnre  11078  ssxr  11206  le2tri3i  11267  muldivdir  11838  0nn0  12443  uzind4  12847  rpnnen1lem5  12922  elfz4  13462  eluzfz  13464  ssfzo12bi  13707  fzoopth  13708  hashgt0elex  14354  hashgt23el  14377  hashxplem  14386  hashfun  14390  ishashinf  14416  wrdsymb1  14506  ccatfv0  14537  lswccats1fst  14589  ccatswrd  14622  ccatpfx  14654  splfv1  14708  cshinj  14764  swrdco  14790  cotr2g  14929  trclun  14967  resqrex  15203  sumeven  16347  ndvdsadd  16370  gcdcllem1  16459  gcdcllem3  16461  lcmftp  16596  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  divgcdcoprmex  16626  1idssfct  16640  prmodvdslcmf  17009  cshwrepswhash1  17064  xpsfrnel2  17519  xpsff1o  17522  catcone0  17644  initoeu2  17974  chnccat  18583  xpsmnd  18736  xpsgrp  19026  mulgfval  19036  gsmsymgrfix  19394  pmtr3ncom  19441  dprdfeq0  19990  gsumdixp  20289  lspcl  20966  lindsind2  21794  lindff1  21795  f1linds  21800  selvcllem5  22115  evls1maplmhm  22363  mat1dimscm  22458  tgcl  22952  elcls  23056  neiptopnei  23115  cmpfii  23392  txcnp  23603  xpstps  23793  fbun  23823  snfil  23847  filconn  23866  isufil2  23891  hauspwpwf1  23970  cnextcn  24050  ustfilxp  24196  ustuqtop4  24227  xpsxms  24517  xpsms  24518  rlmnvc  24686  nmoid  24725  xrsmopn  24796  xrhmeo  24931  cphsqrtcl  25169  iscmet3  25278  iundisj  25533  ioorinv  25561  bddiblnc  25827  dvtaylp  26353  logbid1  26750  logbchbase  26753  relogbcxpb  26769  logbmpt  26770  musum  27172  lgsmodeq  27323  lgsmulsqcoprm  27324  2lgs  27388  2sqnn0  27419  pntlem3  27590  ltsval2  27638  noxp1o  27645  cutbdaylt  27808  zsoring  28419  nb3gr2nb  29471  pthdivtx  29813  pthdlem2lem  29853  crctisclwlk  29880  wwlks  29921  wwlksonvtx  29941  wlkiswwlks2lem1  29955  wwlksnndef  29991  wwlksnfi  29992  clwlkclwwlkf1lem3  30094  clwlkclwwlkf1  30098  clwwlknnn  30121  clwwlkel  30134  wwlksext2clwwlk  30145  clwwlknonwwlknonb  30194  umgr3v3e3cycl  30272  frgrncvvdeq  30397  sspval  30812  blo3i  30891  ajfval  30898  spanval  31422  cmcmlem  31680  leopnmid  32227  csmdsymi  32423  chirredlem4  32482  sumdmdlem  32507  iundisjf  32678  iundisjfi  32888  nn0difffzod  32896  hashxpe  32899  xrpxdivcld  33013  gsumfs2d  33142  fldgensdrg  33398  lsmsnorb  33474  mxidlnzr  33550  zringfrac  33637  lactlmhm  33818  extdgval  33837  ccfldextdgrr  33856  ply1annprmidl  33891  pnfneige0  34135  rrhre  34205  esumcocn  34264  hasheuni  34269  sgon  34308  ddemeas  34420  dya2iocct  34464  dya2iocnrect  34465  eulerpartgbij  34556  eulerpartlemgs2  34564  coinflippv  34668  signstfvneq0  34756  hgt750lemb  34840  bnj1136  35179  bnj1175  35186  bnj1408  35218  fissorduni  35271  fnrelpredd  35272  fineqvnttrclselem1  35302  fineqvnttrclse  35305  unir1regs  35316  axpowg2  35328  axpowg3  35329  onvf1od  35335  vonf1owev  35336  pthhashvtx  35356  spthcycl  35357  upgracycumgr  35381  umgracycusgr  35382  cvmsdisj  35498  mrsubvrs  35750  mppspstlem  35799  problem4  35896  climuzcnv  35899  currybi  35916  dfon2lem7  36015  imageval  36156  filnetlem2  36607  lukshef-ax2  36643  arg-ax  36644  weiunpo  36693  axtco  36699  dfttc4lem2  36757  regsfromunir1  36768  bj-andnotim  36899  bj-modalbe  37031  bj-hbs1  37165  bj-hbsb2av  37167  bj-2uplex  37375  bj-axseprep  37427  mptsnunlem  37700  onsucuni3  37729  finixpnum  37972  fin2solem  37973  matunitlindflem2  37984  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem32  38019  mblfinlem3  38026  itg2addnclem2  38039  itg2addnc  38041  heiborlem3  38180  ismndo2  38241  rngomndo  38302  isfld2  38372  isfldidl  38435  dmncan2  38444  oprabbi  38528  opabbi  38532  ac6s3f  38538  relcnveq3  38694  elrelscnveq3  38994  lsat0cv  39525  djavalN  41627  djhval  41890  dochkr1  41970  dochkr1OLDN  41971  hdmap1fval  42288  lcmineqlem13  42526  fiabv  43022  mhpind  43044  pellexlem5  43278  rmyabs  43403  jm2.24  43408  islssfgi  43517  pwslnm  43539  omlimcl2  43687  onexoegt  43689  rp-oelim2  43753  oeord2lim  43754  oeord2i  43755  ensucne0OLD  43974  iscard5  43980  clrellem  44066  frege114d  44202  frege55lem1a  44310  frege70  44377  gneispace  44578  ismnushort  44745  3impexpbicom  44924  ee3bir  44947  vk15.4j  44972  onfrALTlem2  44990  ax6e2nd  45002  dfvd1impr  45020  dfvd2impr  45048  e1bir  45074  e2bir  45077  e3bir  45182  suctrALT  45269  19.21a3con13vVD  45295  3impexpbicomVD  45300  tratrbVD  45304  ssralv2VD  45309  truniALTVD  45321  trintALTVD  45323  undif3VD  45325  csbingVD  45327  onfrALTlem3VD  45330  onfrALTlem2VD  45332  onfrALTVD  45334  csbsngVD  45336  csbxpgVD  45337  csbrngVD  45339  csbunigVD  45341  csbfv12gALTVD  45342  relopabVD  45344  ax6e2ndVD  45351  2uasbanhVD  45354  vk15.4jVD  45357  sspwimp  45361  sspwimpVD  45362  sspwimpcf  45363  sspwimpcfVD  45364  suctrALTcf  45365  suctrALTcfVD  45366  suctrALT3  45367  sspwimpALT  45368  unisnALT  45369  ax6e2ndALT  45373  isosctrlem1ALT  45377  iunconnlem2  45378  prclaxpr  45429  wfaxrep  45438  supminfxrrnmpt  45914  limsuppnflem  46153  limsupubuz  46156  cncfuni  46329  stoweidlem14  46457  stoweidlem35  46478  stoweidlem57  46500  stirlinglem7  46523  fourierdlem54  46603  etransclem32  46709  subsaliuncl  46801  meadjiunlem  46908  volmea  46917  caratheodory  46971  ovnsubaddlem2  47014  hoidmvlelem5  47042  hoiqssbllem2  47066  aibandbiaiaiffb  47358  funressnvmo  47508  dfdfat2  47591  afvres  47635  ndmaovass  47669  afv2res  47702  tz6.12-afv2  47703  el1fzopredsuc  47789  fundcmpsurinjimaid  47886  iccelpart  47908  lswn0  47919  ichnfimlem  47938  prprelb  47991  indprmfz  48108  evenprm2  48205  dfnbgr6  48348  dfsclnbgr6  48349  isgrtri  48434  grlimedgclnbgr  48486  lincext1  48945  resinsnALT  49363  tposideq  49378  sepfsepc  49418  isclatd  49473  uprcl2  49679  functhincfun  49939  fullthinc  49940  setc2othin  49956