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  biimtrrid  242  imbitrrdi  251  mtbi  322  sylnib  328  simplbi2  500  sylanbr  581  sylan2br  594  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  2541  mo4  2559  nfabdwOLD  2926  r19.30  3119  r19.30OLD  3120  ceqsexv2d  3528  eueq2  3706  ralun  4192  ssunieq  4947  ax6vsep  5303  opelxpi  5713  ordunidif  6413  unizlim  6487  dffo2  6809  dff1o2  6838  resdif  6854  f1o00  6868  fvimacnvALT  7058  fvcofneq  7094  exfo  7106  ressnop0  7153  fsnunfv  7187  ovid  7552  ovidig  7553  dfwe2  7765  dford5  7775  onminex  7794  nnsuc  7877  1stnpr  7983  2ndnpr  7984  f1stres  8003  f2ndres  8004  1st2val  8007  2nd2val  8008  frxp  8117  soxp  8120  frxp2  8135  fprlem1  8291  tz7.49  8451  elixpsn  8937  domdifsn  9060  domunsncan  9078  unfi  9178  cnvfi  9186  fineqvlem  9268  unblem4  9304  ordiso2  9516  zfreg  9596  inf3lem3  9631  trcl  9729  unir1  9814  ssrankr1  9836  djuunxp  9922  pm54.43lem  10001  infxpenlem  10014  ween  10036  acni3  10048  kmlem1  10151  infdif  10210  ackbij1lem1  10221  fin23lem32  10345  isfin1-3  10387  axdc3lem2  10452  ac6c4  10482  zornn0g  10506  axdclem2  10521  rnct  10526  brdom3  10529  brdom5  10530  brdom4  10531  brdom6disj  10533  konigthlem  10569  pwcfsdom  10584  cfpwsdom  10585  alephom  10586  gruina  10819  grur1  10821  grothomex  10830  grothac  10831  nqpr  11015  axcnre  11165  axpre-sup  11170  ssxr  11290  le2tri3i  11351  muldivdir  11914  0nn0  12494  uzind4  12897  rpnnen1lem5  12972  elfz4  13501  eluzfz  13503  ssfzo12bi  13734  hashgt0elex  14368  hashgt23el  14391  hashxplem  14400  hashfun  14404  ishashinf  14431  wrdsymb1  14510  ccatfv0  14540  lswccats1fst  14592  ccatswrd  14625  ccatpfx  14658  splfv1  14712  repswfsts  14738  cshinj  14768  swrdco  14795  cotr2g  14930  trclun  14968  resqrex  15204  sumeven  16337  ndvdsadd  16360  gcdcllem1  16447  gcdcllem3  16449  lcmftp  16580  lcmfunsnlem2lem2  16583  lcmfunsnlem2  16584  lcmfun  16589  coprmprod  16605  coprmproddvdslem  16606  divgcdcoprmex  16610  1idssfct  16624  prmodvdslcmf  16987  cshwrepswhash1  17043  xpsfrnel2  17517  xpsff1o  17520  catcone0  17638  initoeu2  17976  clatlem  18465  clatlubcl2  18467  clatglbcl2  18469  xpsmnd  18705  xpsgrp  18985  mulgfval  18995  gsmsymgrfix  19344  pmtr3ncom  19391  gsumcom3fi  19895  dprdfeq0  19940  gsumdixp  20214  lspcl  20819  lindfind  21682  lindsind  21683  lindsind2  21685  lindff1  21686  f1linds  21691  mat1dimscm  22298  mdetunilem7  22441  fvmptnn04if  22672  tgcl  22793  elcls  22898  opnnei  22945  neiptopnei  22957  cnpnei  23089  cmpfii  23234  txcnp  23445  xpstps  23635  fbun  23665  isfild  23683  snfil  23689  filconn  23708  isufil2  23733  hauspwpwf1  23812  cnextcn  23892  ustfilxp  24038  ustuqtop4  24070  xpsxms  24364  xpsms  24365  rlmnvc  24541  nmoid  24580  xrsmopn  24649  xrhmeo  24792  cphsqrtcl  25033  iscmet3  25142  iundisj  25398  ioorinv  25426  bddiblnc  25692  dvtaylp  26222  logbid1  26615  logbchbase  26618  relogbcxpb  26634  logbmpt  26635  logbfval  26637  musum  27038  lgsmodeq  27190  lgsmulsqcoprm  27191  2lgs  27255  2sqnn0  27286  pntlem3  27457  sltval2  27504  noxp1o  27511  conway  27647  scutbdaylt  27666  nbupgrel  29037  nbusgrvtxm1  29071  nb3gr2nb  29076  pthdivtx  29421  pthdlem2lem  29459  crctisclwlk  29486  wwlks  29524  wwlksonvtx  29544  wspthnonp  29548  wlkiswwlks2lem1  29558  wwlksnndef  29594  wwlksnfi  29595  clwlkclwwlkf1lem3  29694  clwlkclwwlkf1  29698  clwwlknnn  29721  clwwlkel  29734  clwwlkf1  29737  wwlksext2clwwlk  29745  clwwlknonwwlknonb  29794  umgr3v3e3cycl  29872  frgrncvvdeq  29997  sspval  30411  blo3i  30490  ajfval  30497  spanval  31021  cmcmlem  31279  leopnmid  31826  csmdsymi  32022  chirredlem4  32081  sumdmdlem  32106  iundisjf  32255  padct  32379  iundisjfi  32442  nn0difffzod  32451  hashxpe  32454  fprodex01  32466  xrpxdivcld  32536  fldgensdrg  32842  lsmsnorb  32943  mxidlnzr  33025  extdgval  33189  ccfldextdgrr  33203  evls1maplmhm  33217  ply1annprmidl  33225  pnfneige0  33397  rrhre  33467  esumcocn  33544  hasheuni  33549  sgon  33588  sigapildsys  33626  ddemeas  33700  dya2iocct  33745  dya2iocnrect  33746  eulerpartgbij  33837  eulerpartlemgs2  33845  coinflippv  33948  signstfvneq0  34049  hgt750lemb  34134  bnj1136  34474  bnj1175  34481  bnj1408  34513  fnrelpredd  34558  pthhashvtx  34584  spthcycl  34586  upgracycumgr  34610  umgracycusgr  34611  cvmsdisj  34727  mrsubvrs  34979  mppspstlem  35028  problem4  35119  climuzcnv  35122  currybi  35135  dfon2lem7  35233  imageval  35374  filnetlem2  35731  df3nandALT1  35751  lukshef-ax2  35767  arg-ax  35768  bj-andnotim  35933  bj-modalbe  36033  bj-hbs1  36157  bj-hbsb2av  36159  bj-2uplex  36370  mptsnunlem  36686  onsucuni3  36715  fvineqsneq  36760  finixpnum  36940  fin2solem  36941  matunitlindflem2  36952  poimirlem6  36961  poimirlem7  36962  poimirlem8  36963  poimirlem18  36973  poimirlem21  36976  poimirlem22  36977  poimirlem32  36987  mblfinlem3  36994  itg2addnclem2  37007  itg2addnc  37009  ftc1anclem6  37033  heiborlem3  37148  ismndo2  37209  rngomndo  37270  isfld2  37340  isfldidl  37403  dmncan2  37412  oprabbi  37496  opabbi  37500  ac6s3f  37506  relcnveq3  37657  elrelscnveq3  37828  lsat0cv  38370  pclfinclN  39288  docavalN  40461  djavalN  40473  dochval  40689  djhval  40736  dochexmidlem8  40805  dochkr1  40816  dochkr1OLDN  40817  hdmap1fval  41134  lcmineqlem13  41376  selvcllem5  41620  mhpind  41632  pellexlem5  42037  rmyabs  42163  jm2.24  42168  islssfgi  42280  pwslnm  42302  dgraaub  42356  omlimcl2  42457  onexoegt  42459  rp-oelim2  42524  oeord2lim  42525  oeord2i  42526  ensucne0OLD  42747  iscard5  42753  clrellem  42839  frege114d  42975  frege55lem1a  43083  frege70  43150  gneispace  43351  ismnushort  43526  3impexpbicom  43706  ee3bir  43730  vk15.4j  43755  onfrALTlem2  43773  ax6e2nd  43785  dfvd1impr  43803  dfvd2impr  43831  e1bir  43857  e2bir  43860  e3bir  43966  suctrALT  44053  19.21a3con13vVD  44079  3impexpbicomVD  44084  tratrbVD  44088  ssralv2VD  44093  truniALTVD  44105  trintALTVD  44107  undif3VD  44109  csbingVD  44111  onfrALTlem3VD  44114  onfrALTlem2VD  44116  onfrALTVD  44118  csbsngVD  44120  csbxpgVD  44121  csbrngVD  44123  csbunigVD  44125  csbfv12gALTVD  44126  relopabVD  44128  ax6e2ndVD  44135  2uasbanhVD  44138  vk15.4jVD  44141  sspwimp  44145  sspwimpVD  44146  sspwimpcf  44147  sspwimpcfVD  44148  suctrALTcf  44149  suctrALTcfVD  44150  suctrALT3  44151  sspwimpALT  44152  unisnALT  44153  ax6e2ndALT  44157  isosctrlem1ALT  44161  iunconnlem2  44162  supminfxrrnmpt  44643  limsuppnflem  44888  limsupubuz  44891  cncfuni  45064  iblcncfioo  45156  stoweidlem14  45192  stoweidlem17  45195  stoweidlem35  45213  stoweidlem57  45235  stirlinglem7  45258  stirlinglem10  45261  fourierdlem54  45338  fourierdlem62  45346  fourierdlem63  45347  fourierdlem65  45349  fourierdlem73  45357  fourierdlem80  45364  fourierdlem82  45366  fourierdlem101  45385  etransclem32  45444  ioorrnopnxr  45485  subsaliuncl  45536  meadjiunlem  45643  ismeannd  45645  voliunsge0lem  45650  volmea  45652  caratheodory  45706  ovnsubaddlem2  45749  hoidmvlelem5  45777  hoiqssbllem2  45801  iinhoiicc  45852  aibandbiaiaiffb  46067  funressnvmo  46217  dfdfat2  46298  afvres  46342  tz6.12-afv  46343  ndmaovass  46376  afv2res  46409  tz6.12-afv2  46410  el1fzopredsuc  46495  fzoopth  46497  fundcmpsurinjimaid  46541  iccpartiltu  46552  iccelpart  46563  lswn0  46574  ichnfimlem  46593  prprelb  46646  evenprm2  46844  lincext1  47300  sepfsepc  47725  isclatd  47773  intubeu  47774  unilbeu  47775  fullthinc  47831  setc2othin  47841