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  syl6ibr  252  mtbi  322  sylnib  328  simplbi2  502  sylanbr  583  sylan2br  596  pm2.54  851  orbi2i  912  pm2.31  922  pm2.85  932  pm3.11  992  syl3an1br  1407  syl3an2br  1408  syl3an3br  1409  had1  1605  nic-axALT  1677  speimfw  1968  sbbii  2080  hbsbw  2170  mobii  2543  mo4  2561  nfabdwOLD  2928  r19.30  3121  r19.30OLD  3122  ceqsexv2d  3529  eueq2  3706  ralun  4192  ssunieq  4947  ax6vsep  5303  opelxpi  5713  ordunidif  6411  unizlim  6485  dffo2  6807  dff1o2  6836  resdif  6852  f1o00  6866  fvimacnvALT  7056  fvcofneq  7092  exfo  7104  ressnop0  7148  fsnunfv  7182  ovid  7546  ovidig  7547  dfwe2  7758  dford5  7768  onminex  7787  nnsuc  7870  1stnpr  7976  2ndnpr  7977  f1stres  7996  f2ndres  7997  1st2val  8000  2nd2val  8001  frxp  8109  soxp  8112  frxp2  8127  fprlem1  8282  tz7.49  8442  elixpsn  8928  domdifsn  9051  domunsncan  9069  unfi  9169  cnvfi  9177  fineqvlem  9259  unblem4  9295  ordiso2  9507  zfreg  9587  inf3lem3  9622  trcl  9720  unir1  9805  ssrankr1  9827  djuunxp  9913  pm54.43lem  9992  infxpenlem  10005  ween  10027  acni3  10039  kmlem1  10142  infdif  10201  ackbij1lem1  10212  fin23lem32  10336  isfin1-3  10378  axdc3lem2  10443  ac6c4  10473  zornn0g  10497  axdclem2  10512  rnct  10517  brdom3  10520  brdom5  10521  brdom4  10522  brdom6disj  10524  konigthlem  10560  pwcfsdom  10575  cfpwsdom  10576  alephom  10577  gruina  10810  grur1  10812  grothomex  10821  grothac  10822  nqpr  11006  axcnre  11156  axpre-sup  11161  ssxr  11280  le2tri3i  11341  muldivdir  11904  0nn0  12484  uzind4  12887  rpnnen1lem5  12962  elfz4  13491  eluzfz  13493  ssfzo12bi  13724  hashgt0elex  14358  hashgt23el  14381  hashxplem  14390  hashfun  14394  ishashinf  14421  wrdsymb1  14500  ccatfv0  14530  lswccats1fst  14582  ccatswrd  14615  ccatpfx  14648  splfv1  14702  repswfsts  14728  cshinj  14758  swrdco  14785  cotr2g  14920  trclun  14958  resqrex  15194  sumeven  16327  ndvdsadd  16350  gcdcllem1  16437  gcdcllem3  16439  lcmftp  16570  lcmfunsnlem2lem2  16573  lcmfunsnlem2  16574  lcmfun  16579  coprmprod  16595  coprmproddvdslem  16596  divgcdcoprmex  16600  1idssfct  16614  prmodvdslcmf  16977  cshwrepswhash1  17033  xpsfrnel2  17507  xpsff1o  17510  catcone0  17628  initoeu2  17963  clatlem  18452  clatlubcl2  18454  clatglbcl2  18456  xpsmnd  18662  xpsgrp  18939  mulgfval  18947  gsmsymgrfix  19291  pmtr3ncom  19338  gsumcom3fi  19842  dprdfeq0  19887  gsumdixp  20125  lspcl  20580  lindfind  21363  lindsind  21364  lindsind2  21366  lindff1  21367  f1linds  21372  mat1dimscm  21969  mdetunilem7  22112  fvmptnn04if  22343  tgcl  22464  elcls  22569  opnnei  22616  neiptopnei  22628  cnpnei  22760  cmpfii  22905  txcnp  23116  xpstps  23306  fbun  23336  isfild  23354  snfil  23360  filconn  23379  isufil2  23404  hauspwpwf1  23483  cnextcn  23563  ustfilxp  23709  ustuqtop4  23741  xpsxms  24035  xpsms  24036  rlmnvc  24212  nmoid  24251  xrsmopn  24320  xrhmeo  24454  cphsqrtcl  24693  iscmet3  24802  iundisj  25057  ioorinv  25085  bddiblnc  25351  dvtaylp  25874  logbid1  26263  logbchbase  26266  relogbcxpb  26282  logbmpt  26283  logbfval  26285  musum  26685  lgsmodeq  26835  lgsmulsqcoprm  26836  2lgs  26900  2sqnn0  26931  pntlem3  27102  sltval2  27149  noxp1o  27156  conway  27290  scutbdaylt  27309  nbupgrel  28592  nbusgrvtxm1  28626  nb3gr2nb  28631  pthdivtx  28976  pthdlem2lem  29014  crctisclwlk  29041  wwlks  29079  wwlksonvtx  29099  wspthnonp  29103  wlkiswwlks2lem1  29113  wwlksnndef  29149  wwlksnfi  29150  clwlkclwwlkf1lem3  29249  clwlkclwwlkf1  29253  clwwlknnn  29276  clwwlkel  29289  clwwlkf1  29292  wwlksext2clwwlk  29300  clwwlknonwwlknonb  29349  umgr3v3e3cycl  29427  frgrncvvdeq  29552  sspval  29964  blo3i  30043  ajfval  30050  spanval  30574  cmcmlem  30832  leopnmid  31379  csmdsymi  31575  chirredlem4  31634  sumdmdlem  31659  iundisjf  31808  padct  31932  iundisjfi  31995  nn0difffzod  32004  hashxpe  32007  fprodex01  32019  xrpxdivcld  32089  fldgensdrg  32393  lsmsnorb  32490  mxidlnzr  32572  extdgval  32722  ccfldextdgrr  32735  evls1maplmhm  32749  ply1annprmidl  32757  pnfneige0  32920  rrhre  32990  esumcocn  33067  hasheuni  33072  sgon  33111  sigapildsys  33149  ddemeas  33223  dya2iocct  33268  dya2iocnrect  33269  eulerpartgbij  33360  eulerpartlemgs2  33368  coinflippv  33471  signstfvneq0  33572  hgt750lemb  33657  bnj1136  33997  bnj1175  34004  bnj1408  34036  fnrelpredd  34081  pthhashvtx  34107  spthcycl  34109  upgracycumgr  34133  umgracycusgr  34134  cvmsdisj  34250  mrsubvrs  34502  mppspstlem  34551  problem4  34642  climuzcnv  34645  currybi  34658  dfon2lem7  34750  imageval  34891  filnetlem2  35253  df3nandALT1  35273  lukshef-ax2  35289  arg-ax  35290  bj-andnotim  35455  bj-modalbe  35555  bj-hbs1  35679  bj-hbsb2av  35681  bj-2uplex  35892  mptsnunlem  36208  onsucuni3  36237  fvineqsneq  36282  finixpnum  36462  fin2solem  36463  matunitlindflem2  36474  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  poimirlem32  36509  mblfinlem3  36516  itg2addnclem2  36529  itg2addnc  36531  ftc1anclem6  36555  heiborlem3  36670  ismndo2  36731  rngomndo  36792  isfld2  36862  isfldidl  36925  dmncan2  36934  oprabbi  37018  opabbi  37022  ac6s3f  37028  relcnveq3  37179  elrelscnveq3  37350  lsat0cv  37892  pclfinclN  38810  docavalN  39983  djavalN  39995  dochval  40211  djhval  40258  dochexmidlem8  40327  dochkr1  40338  dochkr1OLDN  40339  hdmap1fval  40656  lcmineqlem13  40895  selvcllem5  41152  mhpind  41164  pellexlem5  41557  rmyabs  41683  jm2.24  41688  islssfgi  41800  pwslnm  41822  dgraaub  41876  omlimcl2  41977  onexoegt  41979  rp-oelim2  42044  oeord2lim  42045  oeord2i  42046  ensucne0OLD  42267  iscard5  42273  clrellem  42359  frege114d  42495  frege55lem1a  42603  frege70  42670  gneispace  42871  ismnushort  43046  3impexpbicom  43226  ee3bir  43250  vk15.4j  43275  onfrALTlem2  43293  ax6e2nd  43305  dfvd1impr  43323  dfvd2impr  43351  e1bir  43377  e2bir  43380  e3bir  43486  suctrALT  43573  19.21a3con13vVD  43599  3impexpbicomVD  43604  tratrbVD  43608  ssralv2VD  43613  truniALTVD  43625  trintALTVD  43627  undif3VD  43629  csbingVD  43631  onfrALTlem3VD  43634  onfrALTlem2VD  43636  onfrALTVD  43638  csbsngVD  43640  csbxpgVD  43641  csbrngVD  43643  csbunigVD  43645  csbfv12gALTVD  43646  relopabVD  43648  ax6e2ndVD  43655  2uasbanhVD  43658  vk15.4jVD  43661  sspwimp  43665  sspwimpVD  43666  sspwimpcf  43667  sspwimpcfVD  43668  suctrALTcf  43669  suctrALTcfVD  43670  suctrALT3  43671  sspwimpALT  43672  unisnALT  43673  ax6e2ndALT  43677  isosctrlem1ALT  43681  iunconnlem2  43682  supminfxrrnmpt  44168  limsuppnflem  44413  limsupubuz  44416  cncfuni  44589  iblcncfioo  44681  stoweidlem14  44717  stoweidlem17  44720  stoweidlem35  44738  stoweidlem57  44760  stirlinglem7  44783  stirlinglem10  44786  fourierdlem54  44863  fourierdlem62  44871  fourierdlem63  44872  fourierdlem65  44874  fourierdlem73  44882  fourierdlem80  44889  fourierdlem82  44891  fourierdlem101  44910  etransclem32  44969  ioorrnopnxr  45010  subsaliuncl  45061  meadjiunlem  45168  ismeannd  45170  voliunsge0lem  45175  volmea  45177  caratheodory  45231  ovnsubaddlem2  45274  hoidmvlelem5  45302  hoiqssbllem2  45326  iinhoiicc  45377  aibandbiaiaiffb  45592  funressnvmo  45742  dfdfat2  45823  afvres  45867  tz6.12-afv  45868  ndmaovass  45901  afv2res  45934  tz6.12-afv2  45935  el1fzopredsuc  46020  fzoopth  46022  fundcmpsurinjimaid  46066  iccpartiltu  46077  iccelpart  46088  lswn0  46099  ichnfimlem  46118  prprelb  46171  evenprm2  46369  lincext1  47089  sepfsepc  47514  isclatd  47562  intubeu  47563  unilbeu  47564  fullthinc  47620  setc2othin  47630