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  1603  nic-axALT  1674  speimfw  1963  sbbii  2077  hbsbwOLD  2173  mobii  2541  mo4  2559  r19.30  3100  ceqsexv2dOLD  3500  eueq2  3681  ralun  4161  ssunieq  4907  ax6vsep  5258  opelxpi  5675  ordunidif  6382  unizlim  6457  dffo2  6776  dff1o2  6805  resdif  6821  f1o00  6835  fvimacnvALT  7029  fvcofneq  7065  exfo  7077  ressnop0  7125  fsnunfv  7161  2f1fvneq  7235  ovid  7530  ovidig  7531  dfwe2  7750  dford5  7760  onminex  7778  nnsuc  7860  1stnpr  7972  2ndnpr  7973  f1stres  7992  f2ndres  7993  1st2val  7996  2nd2val  7997  frxp  8105  soxp  8108  frxp2  8123  fprlem1  8279  tz7.49  8413  elixpsn  8910  domdifsn  9024  domunsncan  9041  unfi  9135  cnvfi  9140  fineqvlem  9209  unblem4  9242  ordiso2  9468  zfreg  9548  inf3lem3  9583  trcl  9681  unir1  9766  ssrankr1  9788  djuunxp  9874  pm54.43lem  9953  infxpenlem  9966  ween  9988  acni3  10000  kmlem1  10104  infdif  10161  ackbij1lem1  10172  fin23lem32  10297  isfin1-3  10339  axdc3lem2  10404  ac6c4  10434  zornn0g  10458  axdclem2  10473  rnct  10478  brdom3  10481  brdom5  10482  brdom4  10483  brdom6disj  10485  konigthlem  10521  pwcfsdom  10536  cfpwsdom  10537  alephom  10538  gruina  10771  grur1  10773  grothomex  10782  grothac  10783  nqpr  10967  axcnre  11117  axpre-sup  11122  ssxr  11243  le2tri3i  11304  muldivdir  11875  0nn0  12457  uzind4  12865  rpnnen1lem5  12940  elfz4  13478  eluzfz  13480  ssfzo12bi  13722  fzoopth  13723  hashgt0elex  14366  hashgt23el  14389  hashxplem  14398  hashfun  14402  ishashinf  14428  wrdsymb1  14518  ccatfv0  14548  lswccats1fst  14600  ccatswrd  14633  ccatpfx  14666  splfv1  14720  repswfsts  14746  cshinj  14776  swrdco  14803  cotr2g  14942  trclun  14980  resqrex  15216  sumeven  16357  ndvdsadd  16380  gcdcllem1  16469  gcdcllem3  16471  lcmftp  16606  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfun  16615  coprmprod  16631  coprmproddvdslem  16632  divgcdcoprmex  16636  1idssfct  16650  prmodvdslcmf  17018  cshwrepswhash1  17073  xpsfrnel2  17527  xpsff1o  17530  catcone0  17648  initoeu2  17978  clatlem  18461  clatlubcl2  18463  clatglbcl2  18465  xpsmnd  18704  xpsgrp  18991  mulgfval  19001  gsmsymgrfix  19358  pmtr3ncom  19405  gsumcom3fi  19909  dprdfeq0  19954  gsumdixp  20228  lspcl  20882  lindfind  21725  lindsind  21726  lindsind2  21728  lindff1  21729  f1linds  21734  evls1maplmhm  22264  mat1dimscm  22362  mdetunilem7  22505  fvmptnn04if  22736  tgcl  22856  elcls  22960  opnnei  23007  neiptopnei  23019  cnpnei  23151  cmpfii  23296  txcnp  23507  xpstps  23697  fbun  23727  isfild  23745  snfil  23751  filconn  23770  isufil2  23795  hauspwpwf1  23874  cnextcn  23954  ustfilxp  24100  ustuqtop4  24132  xpsxms  24422  xpsms  24423  rlmnvc  24591  nmoid  24630  xrsmopn  24701  xrhmeo  24844  cphsqrtcl  25084  iscmet3  25193  iundisj  25449  ioorinv  25477  bddiblnc  25743  dvtaylp  26278  logbid1  26678  logbchbase  26681  relogbcxpb  26697  logbmpt  26698  logbfval  26700  musum  27101  lgsmodeq  27253  lgsmulsqcoprm  27254  2lgs  27318  2sqnn0  27349  pntlem3  27520  sltval2  27568  noxp1o  27575  conway  27711  scutbdaylt  27730  nbupgrel  29272  nbusgrvtxm1  29306  nb3gr2nb  29311  pthdivtx  29657  pthdlem2lem  29697  crctisclwlk  29724  wwlks  29765  wwlksonvtx  29785  wspthnonp  29789  wlkiswwlks2lem1  29799  wwlksnndef  29835  wwlksnfi  29836  clwlkclwwlkf1lem3  29935  clwlkclwwlkf1  29939  clwwlknnn  29962  clwwlkel  29975  clwwlkf1  29978  wwlksext2clwwlk  29986  clwwlknonwwlknonb  30035  umgr3v3e3cycl  30113  frgrncvvdeq  30238  sspval  30652  blo3i  30731  ajfval  30738  spanval  31262  cmcmlem  31520  leopnmid  32067  csmdsymi  32263  chirredlem4  32322  sumdmdlem  32347  iundisjf  32518  padct  32643  iundisjfi  32719  nn0difffzod  32729  hashxpe  32732  fprodex01  32750  xrpxdivcld  32855  gsumfs2d  32995  fldgensdrg  33264  lsmsnorb  33362  mxidlnzr  33438  zringfrac  33525  lactlmhm  33630  extdgval  33649  ccfldextdgrr  33667  ply1annprmidl  33697  pnfneige0  33941  rrhre  34011  esumcocn  34070  hasheuni  34075  sgon  34114  sigapildsys  34152  ddemeas  34226  dya2iocct  34271  dya2iocnrect  34272  eulerpartgbij  34363  eulerpartlemgs2  34371  coinflippv  34475  signstfvneq0  34563  hgt750lemb  34647  bnj1136  34987  bnj1175  34994  bnj1408  35026  fnrelpredd  35079  onvf1od  35094  vonf1owev  35095  pthhashvtx  35115  spthcycl  35116  upgracycumgr  35140  umgracycusgr  35141  cvmsdisj  35257  mrsubvrs  35509  mppspstlem  35558  problem4  35655  climuzcnv  35658  currybi  35675  dfon2lem7  35777  imageval  35918  filnetlem2  36367  df3nandALT1  36387  lukshef-ax2  36403  arg-ax  36404  weiunpo  36453  bj-andnotim  36576  bj-modalbe  36676  bj-hbs1  36800  bj-hbsb2av  36802  bj-2uplex  37010  mptsnunlem  37326  onsucuni3  37355  fvineqsneq  37400  finixpnum  37599  fin2solem  37600  matunitlindflem2  37611  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem32  37646  mblfinlem3  37653  itg2addnclem2  37666  itg2addnc  37668  ftc1anclem6  37692  heiborlem3  37807  ismndo2  37868  rngomndo  37929  isfld2  37999  isfldidl  38062  dmncan2  38071  oprabbi  38155  opabbi  38159  ac6s3f  38165  relcnveq3  38309  elrelscnveq3  38482  lsat0cv  39026  pclfinclN  39944  docavalN  41117  djavalN  41129  dochval  41345  djhval  41392  dochexmidlem8  41461  dochkr1  41472  dochkr1OLDN  41473  hdmap1fval  41790  lcmineqlem13  42029  unitscyglem4  42186  fiabv  42524  selvcllem5  42570  mhpind  42582  pellexlem5  42821  rmyabs  42947  jm2.24  42952  islssfgi  43061  pwslnm  43083  dgraaub  43137  omlimcl2  43231  onexoegt  43233  rp-oelim2  43297  oeord2lim  43298  oeord2i  43299  ensucne0OLD  43519  iscard5  43525  clrellem  43611  frege114d  43747  frege55lem1a  43855  frege70  43922  gneispace  44123  ismnushort  44290  3impexpbicom  44470  ee3bir  44493  vk15.4j  44518  onfrALTlem2  44536  ax6e2nd  44548  dfvd1impr  44566  dfvd2impr  44594  e1bir  44620  e2bir  44623  e3bir  44728  suctrALT  44815  19.21a3con13vVD  44841  3impexpbicomVD  44846  tratrbVD  44850  ssralv2VD  44855  truniALTVD  44867  trintALTVD  44869  undif3VD  44871  csbingVD  44873  onfrALTlem3VD  44876  onfrALTlem2VD  44878  onfrALTVD  44880  csbsngVD  44882  csbxpgVD  44883  csbrngVD  44885  csbunigVD  44887  csbfv12gALTVD  44888  relopabVD  44890  ax6e2ndVD  44897  2uasbanhVD  44900  vk15.4jVD  44903  sspwimp  44907  sspwimpVD  44908  sspwimpcf  44909  sspwimpcfVD  44910  suctrALTcf  44911  suctrALTcfVD  44912  suctrALT3  44913  sspwimpALT  44914  unisnALT  44915  ax6e2ndALT  44919  isosctrlem1ALT  44923  iunconnlem2  44924  prclaxpr  44975  wfaxrep  44984  supminfxrrnmpt  45467  limsuppnflem  45708  limsupubuz  45711  cncfuni  45884  iblcncfioo  45976  stoweidlem14  46012  stoweidlem17  46015  stoweidlem35  46033  stoweidlem57  46055  stirlinglem7  46078  stirlinglem10  46081  fourierdlem54  46158  fourierdlem62  46166  fourierdlem63  46167  fourierdlem65  46169  fourierdlem73  46177  fourierdlem80  46184  fourierdlem82  46186  fourierdlem101  46205  etransclem32  46264  ioorrnopnxr  46305  subsaliuncl  46356  meadjiunlem  46463  ismeannd  46465  voliunsge0lem  46470  volmea  46472  caratheodory  46526  ovnsubaddlem2  46569  hoidmvlelem5  46597  hoiqssbllem2  46621  iinhoiicc  46672  aibandbiaiaiffb  46896  funressnvmo  47046  dfdfat2  47129  afvres  47173  tz6.12-afv  47174  ndmaovass  47207  afv2res  47240  tz6.12-afv2  47241  el1fzopredsuc  47326  zp1modne  47347  fundcmpsurinjimaid  47412  iccpartiltu  47423  iccelpart  47434  lswn0  47445  ichnfimlem  47464  prprelb  47517  evenprm2  47715  dfnbgr6  47857  dfsclnbgr6  47858  isgrtri  47942  lincext1  48443  resinsnALT  48861  tposideq  48876  sepfsepc  48916  isclatd  48971  intubeu  48972  unilbeu  48973  uprcl2  49178  functhincfun  49438  fullthinc  49439  setc2othin  49455