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  583  sylan2br  596  pm2.54  853  orbi2i  913  pm2.31  923  pm2.85  933  pm3.11  995  syl3an1br  1409  syl3an2br  1410  syl3an3br  1411  had1  1605  nic-axALT  1676  speimfw  1965  sbbii  2082  hbsbwOLD  2178  mo4  2566  r19.30  3104  ceqsexv2dOLD  3480  eueq2  3656  ralun  4138  ssunieq  4886  replem  5223  ax6vsep  5238  opelxpi  5668  ordunidif  6373  unizlim  6447  dffo2  6756  dff1o2  6785  resdif  6801  f1o00  6815  fvimacnvALT  7009  fvcofneq  7045  exfo  7057  ressnop0  7107  fsnunfv  7142  2f1fvneq  7215  ovid  7508  ovidig  7509  dfwe2  7728  dford5  7738  onminex  7756  nnsuc  7835  1stnpr  7946  2ndnpr  7947  f1stres  7966  f2ndres  7967  1st2val  7970  2nd2val  7971  frxp  8076  soxp  8079  frxp2  8094  fprlem1  8250  tz7.49  8384  elixpsn  8885  domdifsn  8998  domunsncan  9015  unfi  9105  cnvfi  9110  fineqvlem  9176  unblem4  9205  ordiso2  9430  zfreg  9511  elirrv  9512  inf3lem3  9551  trcl  9649  unir1  9737  ssrankr1  9759  djuunxp  9845  pm54.43lem  9924  infxpenlem  9935  ween  9957  acni3  9969  kmlem1  10073  infdif  10130  ackbij1lem1  10141  fin23lem32  10266  isfin1-3  10308  axdc3lem2  10373  ac6c4  10403  zornn0g  10427  axdclem2  10442  rnct  10447  brdom3  10450  brdom5  10451  brdom4  10452  brdom6disj  10454  konigthlem  10491  pwcfsdom  10506  cfpwsdom  10507  alephom  10508  gruina  10741  grur1  10743  grothomex  10752  grothac  10753  nqpr  10937  axcnre  11087  axpre-sup  11092  ssxr  11215  le2tri3i  11276  muldivdir  11847  0nn0  12452  uzind4  12856  rpnnen1lem5  12931  elfz4  13471  eluzfz  13473  ssfzo12bi  13716  fzoopth  13717  hashgt0elex  14363  hashgt23el  14386  hashxplem  14395  hashfun  14399  ishashinf  14425  wrdsymb1  14515  ccatfv0  14546  lswccats1fst  14598  ccatswrd  14631  ccatpfx  14663  splfv1  14717  repswfsts  14743  cshinj  14773  swrdco  14799  cotr2g  14938  trclun  14976  resqrex  15212  sumeven  16356  ndvdsadd  16379  gcdcllem1  16468  gcdcllem3  16470  lcmftp  16605  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfun  16614  coprmprod  16630  coprmproddvdslem  16631  divgcdcoprmex  16635  1idssfct  16649  prmodvdslcmf  17018  cshwrepswhash1  17073  xpsfrnel2  17528  xpsff1o  17531  catcone0  17653  initoeu2  17983  clatlem  18468  clatlubcl2  18470  clatglbcl2  18472  chnccat  18592  xpsmnd  18745  xpsgrp  19035  mulgfval  19045  gsmsymgrfix  19403  pmtr3ncom  19450  gsumcom3fi  19954  dprdfeq0  19999  gsumdixp  20298  lspcl  20971  lindfind  21796  lindsind  21797  lindsind2  21799  lindff1  21800  f1linds  21805  evls1maplmhm  22342  mat1dimscm  22440  mdetunilem7  22583  fvmptnn04if  22814  tgcl  22934  elcls  23038  opnnei  23085  neiptopnei  23097  cnpnei  23229  cmpfii  23374  txcnp  23585  xpstps  23775  fbun  23805  isfild  23823  snfil  23829  filconn  23848  isufil2  23873  hauspwpwf1  23952  cnextcn  24032  ustfilxp  24178  ustuqtop4  24209  xpsxms  24499  xpsms  24500  rlmnvc  24668  nmoid  24707  xrsmopn  24778  xrhmeo  24913  cphsqrtcl  25151  iscmet3  25260  iundisj  25515  ioorinv  25543  bddiblnc  25809  dvtaylp  26335  logbid1  26732  logbchbase  26735  relogbcxpb  26751  logbmpt  26752  logbfval  26754  musum  27154  lgsmodeq  27305  lgsmulsqcoprm  27306  2lgs  27370  2sqnn0  27401  pntlem3  27572  ltsval2  27620  noxp1o  27627  conway  27771  cutbdaylt  27790  zsoring  28401  nbupgrel  29414  nbusgrvtxm1  29448  nb3gr2nb  29453  pthdivtx  29795  pthdlem2lem  29835  crctisclwlk  29862  wwlks  29903  wwlksonvtx  29923  wspthnonp  29927  wlkiswwlks2lem1  29937  wwlksnndef  29973  wwlksnfi  29974  clwlkclwwlkf1lem3  30076  clwlkclwwlkf1  30080  clwwlknnn  30103  clwwlkel  30116  clwwlkf1  30119  wwlksext2clwwlk  30127  clwwlknonwwlknonb  30176  umgr3v3e3cycl  30254  frgrncvvdeq  30379  sspval  30794  blo3i  30873  ajfval  30880  spanval  31404  cmcmlem  31662  leopnmid  32209  csmdsymi  32405  chirredlem4  32464  sumdmdlem  32489  iundisjf  32659  iundisjfi  32869  nn0difffzod  32877  hashxpe  32880  fprodex01  32898  xrpxdivcld  32994  gsumfs2d  33122  fldgensdrg  33375  lsmsnorb  33451  mxidlnzr  33527  zringfrac  33614  lactlmhm  33778  extdgval  33797  ccfldextdgrr  33816  ply1annprmidl  33851  pnfneige0  34095  rrhre  34165  esumcocn  34224  hasheuni  34229  sgon  34268  sigapildsys  34306  ddemeas  34380  dya2iocct  34424  dya2iocnrect  34425  eulerpartgbij  34516  eulerpartlemgs2  34524  coinflippv  34628  signstfvneq0  34716  hgt750lemb  34800  bnj1136  35139  bnj1175  35146  bnj1408  35178  fissorduni  35233  fnrelpredd  35234  fineqvnttrclselem1  35265  fineqvnttrclse  35268  unir1regs  35279  onvf1od  35289  vonf1owev  35290  pthhashvtx  35310  spthcycl  35311  upgracycumgr  35335  umgracycusgr  35336  cvmsdisj  35452  mrsubvrs  35704  mppspstlem  35753  problem4  35850  climuzcnv  35853  currybi  35870  dfon2lem7  35969  imageval  36110  filnetlem2  36561  df3nandALT1  36581  lukshef-ax2  36597  arg-ax  36598  weiunpo  36647  axtco  36653  dfttc4lem2  36711  regsfromunir1  36722  bj-andnotim  36853  bj-modalbe  36985  bj-hbs1  37119  bj-hbsb2av  37121  bj-2uplex  37329  bj-axseprep  37381  mptsnunlem  37654  onsucuni3  37683  fvineqsneq  37728  finixpnum  37926  fin2solem  37927  matunitlindflem2  37938  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem32  37973  mblfinlem3  37980  itg2addnclem2  37993  itg2addnc  37995  ftc1anclem6  38019  heiborlem3  38134  ismndo2  38195  rngomndo  38256  isfld2  38326  isfldidl  38389  dmncan2  38398  oprabbi  38482  opabbi  38486  ac6s3f  38492  relcnveq3  38648  elrelscnveq3  38948  lsat0cv  39479  pclfinclN  40396  docavalN  41569  djavalN  41581  dochval  41797  djhval  41844  dochexmidlem8  41913  dochkr1  41924  dochkr1OLDN  41925  hdmap1fval  42242  lcmineqlem13  42480  unitscyglem4  42637  fiabv  42981  selvcllem5  43015  mhpind  43027  pellexlem5  43261  rmyabs  43386  jm2.24  43391  islssfgi  43500  pwslnm  43522  dgraaub  43576  omlimcl2  43670  onexoegt  43672  rp-oelim2  43736  oeord2lim  43737  oeord2i  43738  ensucne0OLD  43957  iscard5  43963  clrellem  44049  frege114d  44185  frege55lem1a  44293  frege70  44360  gneispace  44561  ismnushort  44728  3impexpbicom  44907  ee3bir  44930  vk15.4j  44955  onfrALTlem2  44973  ax6e2nd  44985  dfvd1impr  45003  dfvd2impr  45031  e1bir  45057  e2bir  45060  e3bir  45165  suctrALT  45252  19.21a3con13vVD  45278  3impexpbicomVD  45283  tratrbVD  45287  ssralv2VD  45292  truniALTVD  45304  trintALTVD  45306  undif3VD  45308  csbingVD  45310  onfrALTlem3VD  45313  onfrALTlem2VD  45315  onfrALTVD  45317  csbsngVD  45319  csbxpgVD  45320  csbrngVD  45322  csbunigVD  45324  csbfv12gALTVD  45325  relopabVD  45327  ax6e2ndVD  45334  2uasbanhVD  45337  vk15.4jVD  45340  sspwimp  45344  sspwimpVD  45345  sspwimpcf  45346  sspwimpcfVD  45347  suctrALTcf  45348  suctrALTcfVD  45349  suctrALT3  45350  sspwimpALT  45351  unisnALT  45352  ax6e2ndALT  45356  isosctrlem1ALT  45360  iunconnlem2  45361  prclaxpr  45412  wfaxrep  45421  supminfxrrnmpt  45899  limsuppnflem  46138  limsupubuz  46141  cncfuni  46314  iblcncfioo  46406  stoweidlem14  46442  stoweidlem17  46445  stoweidlem35  46463  stoweidlem57  46485  stirlinglem7  46508  stirlinglem10  46511  fourierdlem54  46588  fourierdlem62  46596  fourierdlem63  46597  fourierdlem65  46599  fourierdlem73  46607  fourierdlem80  46614  fourierdlem82  46616  fourierdlem101  46635  etransclem32  46694  ioorrnopnxr  46735  subsaliuncl  46786  meadjiunlem  46893  ismeannd  46895  voliunsge0lem  46900  volmea  46902  caratheodory  46956  ovnsubaddlem2  46999  hoidmvlelem5  47027  hoiqssbllem2  47051  iinhoiicc  47102  aibandbiaiaiffb  47343  funressnvmo  47493  dfdfat2  47576  afvres  47620  tz6.12-afv  47621  ndmaovass  47654  afv2res  47687  tz6.12-afv2  47688  el1fzopredsuc  47774  zp1modne  47800  fundcmpsurinjimaid  47871  iccpartiltu  47882  iccelpart  47893  lswn0  47904  ichnfimlem  47923  prprelb  47976  indprmfz  48093  evenprm2  48190  dfnbgr6  48333  dfsclnbgr6  48334  isgrtri  48419  grlimedgclnbgr  48471  lincext1  48930  resinsnALT  49348  tposideq  49363  sepfsepc  49403  isclatd  49458  intubeu  49459  unilbeu  49460  uprcl2  49664  functhincfun  49924  fullthinc  49925  setc2othin  49941