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  2081  hbsbwOLD  2177  mo4  2564  r19.30  3101  ceqsexv2dOLD  3490  eueq2  3666  ralun  4148  ssunieq  4897  ax6vsep  5246  opelxpi  5659  ordunidif  6365  unizlim  6439  dffo2  6748  dff1o2  6777  resdif  6793  f1o00  6807  fvimacnvALT  7000  fvcofneq  7036  exfo  7048  ressnop0  7096  fsnunfv  7131  2f1fvneq  7204  ovid  7497  ovidig  7498  dfwe2  7717  dford5  7727  onminex  7745  nnsuc  7824  1stnpr  7935  2ndnpr  7936  f1stres  7955  f2ndres  7956  1st2val  7959  2nd2val  7960  frxp  8066  soxp  8069  frxp2  8084  fprlem1  8240  tz7.49  8374  elixpsn  8873  domdifsn  8986  domunsncan  9003  unfi  9093  cnvfi  9098  fineqvlem  9164  unblem4  9193  ordiso2  9418  zfreg  9499  elirrv  9500  inf3lem3  9537  trcl  9635  unir1  9723  ssrankr1  9745  djuunxp  9831  pm54.43lem  9910  infxpenlem  9921  ween  9943  acni3  9955  kmlem1  10059  infdif  10116  ackbij1lem1  10127  fin23lem32  10252  isfin1-3  10294  axdc3lem2  10359  ac6c4  10389  zornn0g  10413  axdclem2  10428  rnct  10433  brdom3  10436  brdom5  10437  brdom4  10438  brdom6disj  10440  konigthlem  10477  pwcfsdom  10492  cfpwsdom  10493  alephom  10494  gruina  10727  grur1  10729  grothomex  10738  grothac  10739  nqpr  10923  axcnre  11073  axpre-sup  11078  ssxr  11200  le2tri3i  11261  muldivdir  11832  0nn0  12414  uzind4  12817  rpnnen1lem5  12892  elfz4  13431  eluzfz  13433  ssfzo12bi  13675  fzoopth  13676  hashgt0elex  14322  hashgt23el  14345  hashxplem  14354  hashfun  14358  ishashinf  14384  wrdsymb1  14474  ccatfv0  14505  lswccats1fst  14557  ccatswrd  14590  ccatpfx  14622  splfv1  14676  repswfsts  14702  cshinj  14732  swrdco  14758  cotr2g  14897  trclun  14935  resqrex  15171  sumeven  16312  ndvdsadd  16335  gcdcllem1  16424  gcdcllem3  16426  lcmftp  16561  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  lcmfun  16570  coprmprod  16586  coprmproddvdslem  16587  divgcdcoprmex  16591  1idssfct  16605  prmodvdslcmf  16973  cshwrepswhash1  17028  xpsfrnel2  17483  xpsff1o  17486  catcone0  17608  initoeu2  17938  clatlem  18423  clatlubcl2  18425  clatglbcl2  18427  chnccat  18547  xpsmnd  18700  xpsgrp  18987  mulgfval  18997  gsmsymgrfix  19355  pmtr3ncom  19402  gsumcom3fi  19906  dprdfeq0  19951  gsumdixp  20252  lspcl  20925  lindfind  21769  lindsind  21770  lindsind2  21772  lindff1  21773  f1linds  21778  evls1maplmhm  22319  mat1dimscm  22417  mdetunilem7  22560  fvmptnn04if  22791  tgcl  22911  elcls  23015  opnnei  23062  neiptopnei  23074  cnpnei  23206  cmpfii  23351  txcnp  23562  xpstps  23752  fbun  23782  isfild  23800  snfil  23806  filconn  23825  isufil2  23850  hauspwpwf1  23929  cnextcn  24009  ustfilxp  24155  ustuqtop4  24186  xpsxms  24476  xpsms  24477  rlmnvc  24645  nmoid  24684  xrsmopn  24755  xrhmeo  24898  cphsqrtcl  25138  iscmet3  25247  iundisj  25503  ioorinv  25531  bddiblnc  25797  dvtaylp  26332  logbid1  26732  logbchbase  26735  relogbcxpb  26751  logbmpt  26752  logbfval  26754  musum  27155  lgsmodeq  27307  lgsmulsqcoprm  27308  2lgs  27372  2sqnn0  27403  pntlem3  27574  sltval2  27622  noxp1o  27629  conway  27767  scutbdaylt  27786  zsoring  28367  nbupgrel  29367  nbusgrvtxm1  29401  nb3gr2nb  29406  pthdivtx  29749  pthdlem2lem  29789  crctisclwlk  29816  wwlks  29857  wwlksonvtx  29877  wspthnonp  29881  wlkiswwlks2lem1  29891  wwlksnndef  29927  wwlksnfi  29928  clwlkclwwlkf1lem3  30030  clwlkclwwlkf1  30034  clwwlknnn  30057  clwwlkel  30070  clwwlkf1  30073  wwlksext2clwwlk  30081  clwwlknonwwlknonb  30130  umgr3v3e3cycl  30208  frgrncvvdeq  30333  sspval  30747  blo3i  30826  ajfval  30833  spanval  31357  cmcmlem  31615  leopnmid  32162  csmdsymi  32358  chirredlem4  32417  sumdmdlem  32442  iundisjf  32613  padct  32746  iundisjfi  32825  nn0difffzod  32833  hashxpe  32836  fprodex01  32855  xrpxdivcld  32965  gsumfs2d  33093  fldgensdrg  33345  lsmsnorb  33421  mxidlnzr  33497  zringfrac  33584  lactlmhm  33740  extdgval  33759  ccfldextdgrr  33778  ply1annprmidl  33813  pnfneige0  34057  rrhre  34127  esumcocn  34186  hasheuni  34191  sgon  34230  sigapildsys  34268  ddemeas  34342  dya2iocct  34386  dya2iocnrect  34387  eulerpartgbij  34478  eulerpartlemgs2  34486  coinflippv  34590  signstfvneq0  34678  hgt750lemb  34762  bnj1136  35102  bnj1175  35109  bnj1408  35141  fissorduni  35195  fnrelpredd  35196  fineqvnttrclselem1  35226  fineqvnttrclse  35229  unir1regs  35240  onvf1od  35250  vonf1owev  35251  pthhashvtx  35271  spthcycl  35272  upgracycumgr  35296  umgracycusgr  35297  cvmsdisj  35413  mrsubvrs  35665  mppspstlem  35714  problem4  35811  climuzcnv  35814  currybi  35831  dfon2lem7  35930  imageval  36071  filnetlem2  36522  df3nandALT1  36542  lukshef-ax2  36558  arg-ax  36559  weiunpo  36608  bj-andnotim  36731  bj-modalbe  36832  bj-hbs1  36956  bj-hbsb2av  36958  bj-2uplex  37166  mptsnunlem  37482  onsucuni3  37511  fvineqsneq  37556  finixpnum  37745  fin2solem  37746  matunitlindflem2  37757  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  poimirlem32  37792  mblfinlem3  37799  itg2addnclem2  37812  itg2addnc  37814  ftc1anclem6  37838  heiborlem3  37953  ismndo2  38014  rngomndo  38075  isfld2  38145  isfldidl  38208  dmncan2  38217  oprabbi  38301  opabbi  38305  ac6s3f  38311  relcnveq3  38459  elrelscnveq3  38739  lsat0cv  39232  pclfinclN  40149  docavalN  41322  djavalN  41334  dochval  41550  djhval  41597  dochexmidlem8  41666  dochkr1  41677  dochkr1OLDN  41678  hdmap1fval  41995  lcmineqlem13  42234  unitscyglem4  42391  fiabv  42733  selvcllem5  42767  mhpind  42779  pellexlem5  43017  rmyabs  43142  jm2.24  43147  islssfgi  43256  pwslnm  43278  dgraaub  43332  omlimcl2  43426  onexoegt  43428  rp-oelim2  43492  oeord2lim  43493  oeord2i  43494  ensucne0OLD  43713  iscard5  43719  clrellem  43805  frege114d  43941  frege55lem1a  44049  frege70  44116  gneispace  44317  ismnushort  44484  3impexpbicom  44663  ee3bir  44686  vk15.4j  44711  onfrALTlem2  44729  ax6e2nd  44741  dfvd1impr  44759  dfvd2impr  44787  e1bir  44813  e2bir  44816  e3bir  44921  suctrALT  45008  19.21a3con13vVD  45034  3impexpbicomVD  45039  tratrbVD  45043  ssralv2VD  45048  truniALTVD  45060  trintALTVD  45062  undif3VD  45064  csbingVD  45066  onfrALTlem3VD  45069  onfrALTlem2VD  45071  onfrALTVD  45073  csbsngVD  45075  csbxpgVD  45076  csbrngVD  45078  csbunigVD  45080  csbfv12gALTVD  45081  relopabVD  45083  ax6e2ndVD  45090  2uasbanhVD  45093  vk15.4jVD  45096  sspwimp  45100  sspwimpVD  45101  sspwimpcf  45102  sspwimpcfVD  45103  suctrALTcf  45104  suctrALTcfVD  45105  suctrALT3  45106  sspwimpALT  45107  unisnALT  45108  ax6e2ndALT  45112  isosctrlem1ALT  45116  iunconnlem2  45117  prclaxpr  45168  wfaxrep  45177  supminfxrrnmpt  45657  limsuppnflem  45896  limsupubuz  45899  cncfuni  46072  iblcncfioo  46164  stoweidlem14  46200  stoweidlem17  46203  stoweidlem35  46221  stoweidlem57  46243  stirlinglem7  46266  stirlinglem10  46269  fourierdlem54  46346  fourierdlem62  46354  fourierdlem63  46355  fourierdlem65  46357  fourierdlem73  46365  fourierdlem80  46372  fourierdlem82  46374  fourierdlem101  46393  etransclem32  46452  ioorrnopnxr  46493  subsaliuncl  46544  meadjiunlem  46651  ismeannd  46653  voliunsge0lem  46658  volmea  46660  caratheodory  46714  ovnsubaddlem2  46757  hoidmvlelem5  46785  hoiqssbllem2  46809  iinhoiicc  46860  aibandbiaiaiffb  47083  funressnvmo  47233  dfdfat2  47316  afvres  47360  tz6.12-afv  47361  ndmaovass  47394  afv2res  47427  tz6.12-afv2  47428  el1fzopredsuc  47513  zp1modne  47534  fundcmpsurinjimaid  47599  iccpartiltu  47610  iccelpart  47621  lswn0  47632  ichnfimlem  47651  prprelb  47704  evenprm2  47902  dfnbgr6  48045  dfsclnbgr6  48046  isgrtri  48131  grlimedgclnbgr  48183  lincext1  48642  resinsnALT  49060  tposideq  49075  sepfsepc  49115  isclatd  49170  intubeu  49171  unilbeu  49172  uprcl2  49376  functhincfun  49636  fullthinc  49637  setc2othin  49653