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  1604  nic-axALT  1675  speimfw  1964  sbbii  2079  hbsbwOLD  2175  mobii  2543  mo4  2561  r19.30  3099  ceqsexv2dOLD  3488  eueq2  3664  ralun  4145  ssunieq  4892  ax6vsep  5239  opelxpi  5651  ordunidif  6356  unizlim  6430  dffo2  6739  dff1o2  6768  resdif  6784  f1o00  6798  fvimacnvALT  6990  fvcofneq  7026  exfo  7038  ressnop0  7086  fsnunfv  7121  2f1fvneq  7194  ovid  7487  ovidig  7488  dfwe2  7707  dford5  7717  onminex  7735  nnsuc  7814  1stnpr  7925  2ndnpr  7926  f1stres  7945  f2ndres  7946  1st2val  7949  2nd2val  7950  frxp  8056  soxp  8059  frxp2  8074  fprlem1  8230  tz7.49  8364  elixpsn  8861  domdifsn  8973  domunsncan  8990  unfi  9080  cnvfi  9085  fineqvlem  9150  unblem4  9179  ordiso2  9401  zfreg  9482  elirrv  9483  inf3lem3  9520  trcl  9618  unir1  9706  ssrankr1  9728  djuunxp  9814  pm54.43lem  9893  infxpenlem  9904  ween  9926  acni3  9938  kmlem1  10042  infdif  10099  ackbij1lem1  10110  fin23lem32  10235  isfin1-3  10277  axdc3lem2  10342  ac6c4  10372  zornn0g  10396  axdclem2  10411  rnct  10416  brdom3  10419  brdom5  10420  brdom4  10421  brdom6disj  10423  konigthlem  10459  pwcfsdom  10474  cfpwsdom  10475  alephom  10476  gruina  10709  grur1  10711  grothomex  10720  grothac  10721  nqpr  10905  axcnre  11055  axpre-sup  11060  ssxr  11182  le2tri3i  11243  muldivdir  11814  0nn0  12396  uzind4  12804  rpnnen1lem5  12879  elfz4  13417  eluzfz  13419  ssfzo12bi  13661  fzoopth  13662  hashgt0elex  14308  hashgt23el  14331  hashxplem  14340  hashfun  14344  ishashinf  14370  wrdsymb1  14460  ccatfv0  14491  lswccats1fst  14543  ccatswrd  14576  ccatpfx  14608  splfv1  14662  repswfsts  14688  cshinj  14718  swrdco  14744  cotr2g  14883  trclun  14921  resqrex  15157  sumeven  16298  ndvdsadd  16321  gcdcllem1  16410  gcdcllem3  16412  lcmftp  16547  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  divgcdcoprmex  16577  1idssfct  16591  prmodvdslcmf  16959  cshwrepswhash1  17014  xpsfrnel2  17468  xpsff1o  17471  catcone0  17593  initoeu2  17923  clatlem  18408  clatlubcl2  18410  clatglbcl2  18412  chnccat  18532  xpsmnd  18685  xpsgrp  18972  mulgfval  18982  gsmsymgrfix  19340  pmtr3ncom  19387  gsumcom3fi  19891  dprdfeq0  19936  gsumdixp  20237  lspcl  20909  lindfind  21753  lindsind  21754  lindsind2  21756  lindff1  21757  f1linds  21762  evls1maplmhm  22292  mat1dimscm  22390  mdetunilem7  22533  fvmptnn04if  22764  tgcl  22884  elcls  22988  opnnei  23035  neiptopnei  23047  cnpnei  23179  cmpfii  23324  txcnp  23535  xpstps  23725  fbun  23755  isfild  23773  snfil  23779  filconn  23798  isufil2  23823  hauspwpwf1  23902  cnextcn  23982  ustfilxp  24128  ustuqtop4  24159  xpsxms  24449  xpsms  24450  rlmnvc  24618  nmoid  24657  xrsmopn  24728  xrhmeo  24871  cphsqrtcl  25111  iscmet3  25220  iundisj  25476  ioorinv  25504  bddiblnc  25770  dvtaylp  26305  logbid1  26705  logbchbase  26708  relogbcxpb  26724  logbmpt  26725  logbfval  26727  musum  27128  lgsmodeq  27280  lgsmulsqcoprm  27281  2lgs  27345  2sqnn0  27376  pntlem3  27547  sltval2  27595  noxp1o  27602  conway  27740  scutbdaylt  27759  zsoring  28332  nbupgrel  29323  nbusgrvtxm1  29357  nb3gr2nb  29362  pthdivtx  29705  pthdlem2lem  29745  crctisclwlk  29772  wwlks  29813  wwlksonvtx  29833  wspthnonp  29837  wlkiswwlks2lem1  29847  wwlksnndef  29883  wwlksnfi  29884  clwlkclwwlkf1lem3  29986  clwlkclwwlkf1  29990  clwwlknnn  30013  clwwlkel  30026  clwwlkf1  30029  wwlksext2clwwlk  30037  clwwlknonwwlknonb  30086  umgr3v3e3cycl  30164  frgrncvvdeq  30289  sspval  30703  blo3i  30782  ajfval  30789  spanval  31313  cmcmlem  31571  leopnmid  32118  csmdsymi  32314  chirredlem4  32373  sumdmdlem  32398  iundisjf  32569  padct  32701  iundisjfi  32778  nn0difffzod  32786  hashxpe  32789  fprodex01  32808  xrpxdivcld  32915  gsumfs2d  33035  fldgensdrg  33280  lsmsnorb  33356  mxidlnzr  33432  zringfrac  33519  lactlmhm  33647  extdgval  33666  ccfldextdgrr  33685  ply1annprmidl  33720  pnfneige0  33964  rrhre  34034  esumcocn  34093  hasheuni  34098  sgon  34137  sigapildsys  34175  ddemeas  34249  dya2iocct  34293  dya2iocnrect  34294  eulerpartgbij  34385  eulerpartlemgs2  34393  coinflippv  34497  signstfvneq0  34585  hgt750lemb  34669  bnj1136  35009  bnj1175  35016  bnj1408  35048  fissorduni  35101  fnrelpredd  35102  unir1regs  35131  fineqvnttrclselem1  35141  fineqvnttrclse  35144  onvf1od  35151  vonf1owev  35152  pthhashvtx  35172  spthcycl  35173  upgracycumgr  35197  umgracycusgr  35198  cvmsdisj  35314  mrsubvrs  35566  mppspstlem  35615  problem4  35712  climuzcnv  35715  currybi  35732  dfon2lem7  35831  imageval  35972  filnetlem2  36421  df3nandALT1  36441  lukshef-ax2  36457  arg-ax  36458  weiunpo  36507  bj-andnotim  36630  bj-modalbe  36730  bj-hbs1  36854  bj-hbsb2av  36856  bj-2uplex  37064  mptsnunlem  37380  onsucuni3  37409  fvineqsneq  37454  finixpnum  37653  fin2solem  37654  matunitlindflem2  37665  poimirlem6  37674  poimirlem7  37675  poimirlem8  37676  poimirlem18  37686  poimirlem21  37689  poimirlem22  37690  poimirlem32  37700  mblfinlem3  37707  itg2addnclem2  37720  itg2addnc  37722  ftc1anclem6  37746  heiborlem3  37861  ismndo2  37922  rngomndo  37983  isfld2  38053  isfldidl  38116  dmncan2  38125  oprabbi  38209  opabbi  38213  ac6s3f  38219  relcnveq3  38363  elrelscnveq3  38536  lsat0cv  39080  pclfinclN  39997  docavalN  41170  djavalN  41182  dochval  41398  djhval  41445  dochexmidlem8  41514  dochkr1  41525  dochkr1OLDN  41526  hdmap1fval  41843  lcmineqlem13  42082  unitscyglem4  42239  fiabv  42577  selvcllem5  42623  mhpind  42635  pellexlem5  42874  rmyabs  42999  jm2.24  43004  islssfgi  43113  pwslnm  43135  dgraaub  43189  omlimcl2  43283  onexoegt  43285  rp-oelim2  43349  oeord2lim  43350  oeord2i  43351  ensucne0OLD  43571  iscard5  43577  clrellem  43663  frege114d  43799  frege55lem1a  43907  frege70  43974  gneispace  44175  ismnushort  44342  3impexpbicom  44521  ee3bir  44544  vk15.4j  44569  onfrALTlem2  44587  ax6e2nd  44599  dfvd1impr  44617  dfvd2impr  44645  e1bir  44671  e2bir  44674  e3bir  44779  suctrALT  44866  19.21a3con13vVD  44892  3impexpbicomVD  44897  tratrbVD  44901  ssralv2VD  44906  truniALTVD  44918  trintALTVD  44920  undif3VD  44922  csbingVD  44924  onfrALTlem3VD  44927  onfrALTlem2VD  44929  onfrALTVD  44931  csbsngVD  44933  csbxpgVD  44934  csbrngVD  44936  csbunigVD  44938  csbfv12gALTVD  44939  relopabVD  44941  ax6e2ndVD  44948  2uasbanhVD  44951  vk15.4jVD  44954  sspwimp  44958  sspwimpVD  44959  sspwimpcf  44960  sspwimpcfVD  44961  suctrALTcf  44962  suctrALTcfVD  44963  suctrALT3  44964  sspwimpALT  44965  unisnALT  44966  ax6e2ndALT  44970  isosctrlem1ALT  44974  iunconnlem2  44975  prclaxpr  45026  wfaxrep  45035  supminfxrrnmpt  45517  limsuppnflem  45756  limsupubuz  45759  cncfuni  45932  iblcncfioo  46024  stoweidlem14  46060  stoweidlem17  46063  stoweidlem35  46081  stoweidlem57  46103  stirlinglem7  46126  stirlinglem10  46129  fourierdlem54  46206  fourierdlem62  46214  fourierdlem63  46215  fourierdlem65  46217  fourierdlem73  46225  fourierdlem80  46232  fourierdlem82  46234  fourierdlem101  46253  etransclem32  46312  ioorrnopnxr  46353  subsaliuncl  46404  meadjiunlem  46511  ismeannd  46513  voliunsge0lem  46518  volmea  46520  caratheodory  46574  ovnsubaddlem2  46617  hoidmvlelem5  46645  hoiqssbllem2  46669  iinhoiicc  46720  aibandbiaiaiffb  46934  funressnvmo  47084  dfdfat2  47167  afvres  47211  tz6.12-afv  47212  ndmaovass  47245  afv2res  47278  tz6.12-afv2  47279  el1fzopredsuc  47364  zp1modne  47385  fundcmpsurinjimaid  47450  iccpartiltu  47461  iccelpart  47472  lswn0  47483  ichnfimlem  47502  prprelb  47555  evenprm2  47753  dfnbgr6  47896  dfsclnbgr6  47897  isgrtri  47982  grlimedgclnbgr  48034  lincext1  48494  resinsnALT  48912  tposideq  48927  sepfsepc  48967  isclatd  49022  intubeu  49023  unilbeu  49024  uprcl2  49229  functhincfun  49489  fullthinc  49490  setc2othin  49506