Theorem biimpri 227

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mpbir  230  sylibr  233  sylbir  234  sylbbr  235  sylbb1  236  sylbb2  237  syl5bir  242  syl6ibr  251  mtbi  321  sylnib  327  simplbi2  501  sylanbr  582  sylan2br  595  pm2.54  849  orbi2i  910  pm2.31  920  pm2.85  930  pm3.11  990  syl3an1br  1405  syl3an2br  1406  syl3an3br  1407  had1  1603  nic-axALT  1675  speimfw  1966  sbbii  2078  hbsbw  2168  mobii  2546  mo4  2564  nfabdwOLD  2928  r19.30  3119  r19.30OLD  3120  ceqsexv2d  3490  eueq2  3656  ralun  4140  ssunieq  4892  ax6vsep  5248  opelxpi  5658  ordunidif  6351  unizlim  6424  dffo2  6744  dff1o2  6773  resdif  6789  f1o00  6803  fvimacnvALT  6991  fvcofneq  7026  exfo  7038  ressnop0  7082  fsnunfv  7116  ovid  7477  ovidig  7478  dfwe2  7687  dford5  7697  onminex  7716  nnsuc  7799  1stnpr  7904  2ndnpr  7905  f1stres  7924  f2ndres  7925  1st2val  7928  2nd2val  7929  frxp  8035  soxp  8038  fprlem1  8187  tz7.49  8347  elixpsn  8797  domdifsn  8920  domunsncan  8938  unfi  9038  cnvfi  9046  fineqvlem  9128  unblem4  9164  ordiso2  9373  zfreg  9453  inf3lem3  9488  trcl  9586  unir1  9671  ssrankr1  9693  djuunxp  9779  pm54.43lem  9858  infxpenlem  9871  ween  9893  acni3  9905  kmlem1  10008  infdif  10067  ackbij1lem1  10078  fin23lem32  10202  isfin1-3  10244  axdc3lem2  10309  ac6c4  10339  zornn0g  10363  axdclem2  10378  rnct  10383  brdom3  10386  brdom5  10387  brdom4  10388  brdom6disj  10390  konigthlem  10426  pwcfsdom  10441  cfpwsdom  10442  alephom  10443  gruina  10676  grur1  10678  grothomex  10687  grothac  10688  nqpr  10872  axcnre  11022  axpre-sup  11027  ssxr  11146  le2tri3i  11207  muldivdir  11770  0nn0  12350  uzind4  12748  rpnnen1lem5  12823  elfz4  13351  eluzfz  13353  ssfzo12bi  13584  hashgt0elex  14217  hashgt23el  14240  hashxplem  14249  hashfun  14253  ishashinf  14278  wrdsymb1  14357  ccatfv0  14388  lswccats1fst  14444  ccatswrd  14480  ccatpfx  14513  splfv1  14567  repswfsts  14593  cshinj  14623  swrdco  14650  cotr2g  14787  trclun  14825  resqrex  15062  sumeven  16196  ndvdsadd  16219  gcdcllem1  16306  gcdcllem3  16308  lcmftp  16439  lcmfunsnlem2lem2  16442  lcmfunsnlem2  16443  lcmfun  16448  coprmprod  16464  coprmproddvdslem  16465  divgcdcoprmex  16469  1idssfct  16483  prmodvdslcmf  16846  cshwrepswhash1  16902  xpsfrnel2  17373  xpsff1o  17376  catcone0  17494  initoeu2  17829  clatlem  18318  clatlubcl2  18320  clatglbcl2  18322  xpsmnd  18523  xpsgrp  18791  mulgfval  18799  gsmsymgrfix  19133  pmtr3ncom  19180  gsumcom3fi  19676  dprdfeq0  19721  gsumdixp  19944  lspcl  20345  lindfind  21130  lindsind  21131  lindsind2  21133  lindff1  21134  f1linds  21139  mat1dimscm  21731  mdetunilem7  21874  fvmptnn04if  22105  tgcl  22226  elcls  22331  opnnei  22378  neiptopnei  22390  cnpnei  22522  cmpfii  22667  txcnp  22878  xpstps  23068  fbun  23098  isfild  23116  snfil  23122  filconn  23141  isufil2  23166  hauspwpwf1  23245  cnextcn  23325  ustfilxp  23471  ustuqtop4  23503  xpsxms  23797  xpsms  23798  rlmnvc  23974  nmoid  24013  xrsmopn  24082  xrhmeo  24216  cphsqrtcl  24455  iscmet3  24564  iundisj  24819  ioorinv  24847  bddiblnc  25113  dvtaylp  25636  logbid1  26025  logbchbase  26028  relogbcxpb  26044  logbmpt  26045  logbfval  26047  musum  26447  lgsmodeq  26597  lgsmulsqcoprm  26598  2lgs  26662  2sqnn0  26693  pntlem3  26864  sltval2  26911  noxp1o  26918  conway  27045  scutbdaylt  27064  nbupgrel  28002  nbusgrvtxm1  28036  nb3gr2nb  28041  pthdivtx  28386  pthdlem2lem  28424  crctisclwlk  28451  wwlks  28489  wwlksonvtx  28509  wspthnonp  28513  wlkiswwlks2lem1  28523  wwlksnndef  28559  wwlksnfi  28560  clwlkclwwlkf1lem3  28659  clwlkclwwlkf1  28663  clwwlknnn  28686  clwwlkel  28699  clwwlkf1  28702  wwlksext2clwwlk  28710  clwwlknonwwlknonb  28759  umgr3v3e3cycl  28837  frgrncvvdeq  28962  sspval  29374  blo3i  29453  ajfval  29460  spanval  29984  cmcmlem  30242  leopnmid  30789  csmdsymi  30985  chirredlem4  31044  sumdmdlem  31069  iundisjf  31215  padct  31341  iundisjfi  31404  hashxpe  31414  fprodex01  31426  xrpxdivcld  31496  fldgensdrg  31787  lsmsnorb  31876  mxidlnzr  31936  extdgval  32027  ccfldextdgrr  32040  pnfneige0  32199  rrhre  32269  esumcocn  32346  hasheuni  32351  sgon  32390  sigapildsys  32428  ddemeas  32502  dya2iocct  32547  dya2iocnrect  32548  eulerpartgbij  32639  eulerpartlemgs2  32647  coinflippv  32750  signstfvneq0  32851  hgt750lemb  32936  bnj1136  33276  bnj1175  33283  bnj1408  33315  fnrelpredd  33360  pthhashvtx  33388  spthcycl  33390  upgracycumgr  33414  umgracycusgr  33415  cvmsdisj  33531  mrsubvrs  33783  mppspstlem  33832  problem4  33925  climuzcnv  33928  dfon2lem7  34050  frxp2  34075  imageval  34371  filnetlem2  34707  df3nandALT1  34727  lukshef-ax2  34743  arg-ax  34744  bj-andnotim  34909  bj-modalbe  35009  bj-hbs1  35133  bj-hbsb2av  35135  bj-2uplex  35349  mptsnunlem  35665  onsucuni3  35694  fvineqsneq  35739  finixpnum  35918  fin2solem  35919  matunitlindflem2  35930  poimirlem6  35939  poimirlem7  35940  poimirlem8  35941  poimirlem18  35951  poimirlem21  35954  poimirlem22  35955  poimirlem32  35965  mblfinlem3  35972  itg2addnclem2  35985  itg2addnc  35987  ftc1anclem6  36011  heiborlem3  36127  ismndo2  36188  rngomndo  36249  isfld2  36319  isfldidl  36382  dmncan2  36391  oprabbi  36475  opabbi  36479  ac6s3f  36485  relcnveq3  36638  elrelscnveq3  36809  lsat0cv  37351  pclfinclN  38269  docavalN  39442  djavalN  39454  dochval  39670  djhval  39717  dochexmidlem8  39786  dochkr1  39797  dochkr1OLDN  39798  hdmap1fval  40115  lcmineqlem13  40354  selvval2lem5  40534  mhpind  40594  pellexlem5  40968  rmyabs  41094  jm2.24  41099  islssfgi  41211  pwslnm  41233  dgraaub  41287  omlimcl2  41363  ensucne0OLD  41511  iscard5  41517  clrellem  41603  frege114d  41739  frege55lem1a  41847  frege70  41914  gneispace  42117  ismnushort  42292  3impexpbicom  42472  ee3bir  42496  vk15.4j  42521  onfrALTlem2  42539  ax6e2nd  42551  dfvd1impr  42569  dfvd2impr  42597  e1bir  42623  e2bir  42626  e3bir  42732  suctrALT  42819  19.21a3con13vVD  42845  3impexpbicomVD  42850  tratrbVD  42854  ssralv2VD  42859  truniALTVD  42871  trintALTVD  42873  undif3VD  42875  onfrALTlem3VD  42880  onfrALTlem2VD  42882  onfrALTVD  42884  relopabVD  42894  ax6e2ndVD  42901  2uasbanhVD  42904  vk15.4jVD  42907  sspwimp  42911  sspwimpVD  42912  sspwimpcf  42913  sspwimpcfVD  42914  suctrALTcf  42915  suctrALTcfVD  42916  suctrALT3  42917  sspwimpALT  42918  unisnALT  42919  ax6e2ndALT  42923  isosctrlem1ALT  42927  iunconnlem2  42928  supminfxrrnmpt  43398  limsuppnflem  43639  limsupubuz  43642  cncfuni  43815  iblcncfioo  43907  stoweidlem14  43943  stoweidlem17  43946  stoweidlem35  43964  stoweidlem57  43986  stirlinglem7  44009  stirlinglem10  44012  fourierdlem54  44089  fourierdlem62  44097  fourierdlem63  44098  fourierdlem65  44100  fourierdlem73  44108  fourierdlem80  44115  fourierdlem82  44117  fourierdlem101  44136  etransclem32  44195  ioorrnopnxr  44236  subsaliuncl  44285  meadjiunlem  44392  ismeannd  44394  voliunsge0lem  44399  volmea  44401  caratheodory  44455  ovnsubaddlem2  44498  hoidmvlelem5  44526  hoiqssbllem2  44550  iinhoiicc  44601  aibandbiaiaiffb  44808  funressnvmo  44957  dfdfat2  45038  afvres  45082  tz6.12-afv  45083  ndmaovass  45116  afv2res  45149  tz6.12-afv2  45150  el1fzopredsuc  45235  fzoopth  45237  fundcmpsurinjimaid  45281  iccpartiltu  45292  iccelpart  45303  lswn0  45314  ichnfimlem  45333  prprelb  45386  evenprm2  45584  lincext1  46213  sepfsepc  46639  isclatd  46687  intubeu  46688  unilbeu  46689  fullthinc  46745  setc2othin  46755