Theorem biimpri 230

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  mpbir  233  sylibr  236  sylbir  237  sylbbr  238  sylbb1  239  sylbb2  240  syl5bir  245  syl6ibr  254  mtbi  324  sylnib  330  simplbi2  503  sylanbr  584  sylan2br  596  pm2.54  848  orbi2i  909  pm2.31  919  pm2.85  929  pm3.11  989  syl3an1br  1402  syl3an2br  1403  syl3an3br  1404  had1  1604  nic-axALT  1675  speimfw  1966  sbbii  2081  sb2vOLD  2097  sbbiiALT  2578  mobii  2631  mo4  2650  nfabdw  3000  r19.30  3338  ceqsexv2d  3542  eueq2  3701  ralun  4168  ssunieq  4873  ax6vsep  5207  opelxpi  5592  ordunidif  6239  unizlim  6307  dffo2  6594  dff1o2  6620  resdif  6635  f1o00  6649  fvimacnvALT  6827  fvcofneq  6859  exfo  6871  ressnop0  6915  fsnunfv  6949  ovid  7291  ovidig  7292  dfwe2  7496  onminex  7522  nnsuc  7597  1stnpr  7693  2ndnpr  7694  f1stres  7713  f2ndres  7714  1st2val  7717  2nd2val  7718  frxp  7820  soxp  7823  tz7.49  8081  elixpsn  8501  domdifsn  8600  domunsncan  8617  fineqvlem  8732  unblem4  8773  ordiso2  8979  zfreg  9059  inf3lem3  9093  trcl  9170  unir1  9242  ssrankr1  9264  djuunxp  9350  pm54.43lem  9428  infxpenlem  9439  ween  9461  acni3  9473  kmlem1  9576  infdif  9631  ackbij1lem1  9642  fin23lem32  9766  isfin1-3  9808  axdc3lem2  9873  ac6c4  9903  zornn0g  9927  axdclem2  9942  rnct  9947  brdom3  9950  brdom5  9951  brdom4  9952  brdom6disj  9954  konigthlem  9990  pwcfsdom  10005  cfpwsdom  10006  alephom  10007  gruina  10240  grur1  10242  grothomex  10251  grothac  10252  nqpr  10436  axcnre  10586  axpre-sup  10591  ssxr  10710  le2tri3i  10770  muldivdir  11333  0nn0  11913  uzind4  12307  rpnnen1lem5  12381  elfz4  12902  eluzfz  12904  ssfzo12bi  13133  hashgt0elex  13763  hashgt23el  13786  hashxplem  13795  hashfun  13799  ishashinf  13822  ffz0iswrdOLD  13892  wrdsymb1  13905  ccatfv0  13937  lswccats1fst  13994  ccatswrd  14030  ccatpfx  14063  splfv1  14117  repswfsts  14143  cshinj  14173  swrdco  14199  cotr2g  14336  trclun  14374  resqrex  14610  pwm1geoserOLD  15225  sumeven  15738  ndvdsadd  15761  gcdcllem1  15848  gcdcllem3  15850  lcmftp  15980  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  divgcdcoprmex  16010  1idssfct  16024  prmodvdslcmf  16383  cshwrepswhash1  16436  xpsfrnel2  16837  xpsff1o  16840  initoeu2  17276  clatlem  17721  clatlubcl2  17723  clatglbcl2  17725  xpsmnd  17951  xpsgrp  18218  mulgfval  18226  gsmsymgrfix  18556  pmtr3ncom  18603  gsumcom3fi  19099  dprdfeq0  19144  gsumdixp  19359  lspcl  19748  lindfind  20960  lindsind  20961  lindsind2  20963  lindff1  20964  f1linds  20969  mat1dimscm  21084  mdetunilem7  21227  fvmptnn04if  21457  tgcl  21577  elcls  21681  opnnei  21728  neiptopnei  21740  cnpnei  21872  cmpfii  22017  txcnp  22228  xpstps  22418  fbun  22448  isfild  22466  snfil  22472  filconn  22491  isufil2  22516  hauspwpwf1  22595  cnextcn  22675  ustfilxp  22821  ustuqtop4  22853  xpsxms  23144  xpsms  23145  rlmnvc  23312  nmoid  23351  xrsmopn  23420  xrhmeo  23550  cphsqrtcl  23788  iscmet3  23896  iundisj  24149  ioorinv  24177  dvtaylp  24958  logbid1  25346  logbchbase  25349  relogbcxpb  25365  logbmpt  25366  logbfval  25368  musum  25768  lgsmodeq  25918  lgsmulsqcoprm  25919  2lgs  25983  2sqnn0  26014  pntlem3  26185  nbupgrel  27127  nbusgrvtxm1  27161  nb3gr2nb  27166  pthdivtx  27510  pthdlem2lem  27548  crctisclwlk  27575  wwlks  27613  wwlksonvtx  27633  wspthnonp  27637  wlkiswwlks2lem1  27647  wwlksnndef  27683  wwlksnfi  27684  clwlkclwwlkf1lem3  27784  clwlkclwwlkf1  27788  clwwlknnn  27811  clwwlknfiOLD  27824  clwwlkel  27825  clwwlkf1  27828  wwlksext2clwwlk  27836  clwwlknonwwlknonb  27885  umgr3v3e3cycl  27963  frgrncvvdeq  28088  sspval  28500  blo3i  28579  ajfval  28586  spanval  29110  cmcmlem  29368  leopnmid  29915  csmdsymi  30111  chirredlem4  30170  sumdmdlem  30195  iundisjf  30339  padct  30455  iundisjfi  30519  hashxpe  30529  fprodex01  30541  xrpxdivcld  30611  wrdt2ind  30627  lsmsnorb  30945  mxidlnzr  30976  extdgval  31044  ccfldextdgrr  31057  pnfneige0  31194  rrhre  31262  esumcocn  31339  hasheuni  31344  sgon  31383  sigapildsys  31421  ddemeas  31495  dya2iocct  31538  dya2iocnrect  31539  eulerpartgbij  31630  eulerpartlemgs2  31638  coinflippv  31741  signstfvneq0  31842  hgt750lemb  31927  bnj1136  32269  bnj1175  32276  bnj1408  32308  pthhashvtx  32374  spthcycl  32376  upgracycumgr  32400  umgracycusgr  32401  cvmsdisj  32517  mrsubvrs  32769  mppspstlem  32818  problem4  32911  climuzcnv  32914  dford5  32957  dfon2lem7  33034  fprlem1  33137  sltval2  33163  noxp1o  33170  conway  33264  scutbdaylt  33276  imageval  33391  filnetlem2  33727  df3nandALT1  33747  lukshef-ax2  33763  arg-ax  33764  bj-andnotim  33922  bj-modalbe  34022  bj-hbs1  34134  bj-hbsb2av  34136  bj-2uplex  34337  mptsnunlem  34622  onsucuni3  34651  fvineqsneq  34696  finixpnum  34892  fin2solem  34893  matunitlindflem2  34904  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem32  34939  mblfinlem3  34946  itg2addnclem2  34959  itg2addnc  34961  bddiblnc  34977  ftc1anclem6  34987  heiborlem3  35106  ismndo2  35167  rngomndo  35228  isfld2  35298  isfldidl  35361  dmncan2  35370  oprabbi  35454  opabbi  35458  ac6s3f  35464  relcnveq3  35593  elrelscnveq3  35746  lsat0cv  36184  pclfinclN  37101  docavalN  38274  djavalN  38286  dochval  38502  djhval  38549  dochexmidlem8  38618  dochkr1  38629  dochkr1OLDN  38630  hdmap1fval  38947  selvval2lem5  39157  pellexlem5  39450  rmyabs  39575  jm2.24  39580  islssfgi  39692  pwslnm  39714  dgraaub  39768  ensucne0OLD  39916  iscard5  39921  clrellem  40002  frege114d  40123  frege55lem1a  40232  frege70  40299  gneispace  40504  3impexpbicom  40833  ee3bir  40857  vk15.4j  40882  onfrALTlem2  40900  ax6e2nd  40912  dfvd1impr  40930  dfvd2impr  40958  e1bir  40984  e2bir  40987  e3bir  41093  suctrALT  41180  19.21a3con13vVD  41206  3impexpbicomVD  41211  tratrbVD  41215  ssralv2VD  41220  truniALTVD  41232  trintALTVD  41234  undif3VD  41236  onfrALTlem3VD  41241  onfrALTlem2VD  41243  onfrALTVD  41245  relopabVD  41255  ax6e2ndVD  41262  2uasbanhVD  41265  vk15.4jVD  41268  sspwimp  41272  sspwimpVD  41273  sspwimpcf  41274  sspwimpcfVD  41275  suctrALTcf  41276  suctrALTcfVD  41277  suctrALT3  41278  sspwimpALT  41279  unisnALT  41280  ax6e2ndALT  41284  isosctrlem1ALT  41288  iunconnlem2  41289  supminfxrrnmpt  41767  limsuppnflem  42011  limsupubuz  42014  cncfuni  42189  iblcncfioo  42283  stoweidlem14  42319  stoweidlem17  42322  stoweidlem35  42340  stoweidlem57  42362  stirlinglem7  42385  stirlinglem10  42388  fourierdlem54  42465  fourierdlem62  42473  fourierdlem63  42474  fourierdlem65  42476  fourierdlem73  42484  fourierdlem80  42491  fourierdlem82  42493  fourierdlem101  42512  etransclem32  42571  ioorrnopnxr  42612  subsaliuncl  42661  meadjiunlem  42767  ismeannd  42769  voliunsge0lem  42774  volmea  42776  caratheodory  42830  ovnsubaddlem2  42873  hoidmvlelem5  42901  hoiqssbllem2  42925  iinhoiicc  42976  aibandbiaiaiffb  43151  funressnvmo  43300  dfdfat2  43347  afvres  43391  tz6.12-afv  43392  ndmaovass  43425  afv2res  43458  tz6.12-afv2  43459  el1fzopredsuc  43545  fzoopth  43547  fundcmpsurinjimaid  43591  iccpartiltu  43602  iccelpart  43613  lswn0  43624  prprelb  43698  evenprm2  43899  lincext1  44529