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  321  sylnib  327  simplbi2  499  sylanbr  580  sylan2br  593  pm2.54  850  orbi2i  910  pm2.31  920  pm2.85  930  pm3.11  990  syl3an1br  1403  syl3an2br  1404  syl3an3br  1405  had1  1596  nic-axALT  1668  speimfw  1959  sbbii  2071  hbsbwOLD  2161  mobii  2536  mo4  2554  nfabdwOLD  2916  r19.30  3109  r19.30OLD  3110  ceqsexv2dOLD  3518  eueq2  3702  ralun  4190  ssunieq  4947  ax6vsep  5304  opelxpi  5715  ordunidif  6420  unizlim  6494  dffo2  6814  dff1o2  6843  resdif  6859  f1o00  6873  fvimacnvALT  7065  fvcofneq  7102  exfo  7114  ressnop0  7162  fsnunfv  7196  ovid  7562  ovidig  7563  dfwe2  7777  dford5  7787  onminex  7806  nnsuc  7889  1stnpr  7998  2ndnpr  7999  f1stres  8018  f2ndres  8019  1st2val  8022  2nd2val  8023  frxp  8131  soxp  8134  frxp2  8149  fprlem1  8306  tz7.49  8466  elixpsn  8956  domdifsn  9079  domunsncan  9097  unfi  9197  cnvfi  9205  fineqvlem  9287  unblem4  9323  ordiso2  9540  zfreg  9620  inf3lem3  9655  trcl  9753  unir1  9838  ssrankr1  9860  djuunxp  9946  pm54.43lem  10025  infxpenlem  10038  ween  10060  acni3  10072  kmlem1  10175  infdif  10234  ackbij1lem1  10245  fin23lem32  10369  isfin1-3  10411  axdc3lem2  10476  ac6c4  10506  zornn0g  10530  axdclem2  10545  rnct  10550  brdom3  10553  brdom5  10554  brdom4  10555  brdom6disj  10557  konigthlem  10593  pwcfsdom  10608  cfpwsdom  10609  alephom  10610  gruina  10843  grur1  10845  grothomex  10854  grothac  10855  nqpr  11039  axcnre  11189  axpre-sup  11194  ssxr  11315  le2tri3i  11376  muldivdir  11940  0nn0  12520  uzind4  12923  rpnnen1lem5  12998  elfz4  13529  eluzfz  13531  ssfzo12bi  13762  fzoopth  13763  hashgt0elex  14396  hashgt23el  14419  hashxplem  14428  hashfun  14432  ishashinf  14460  wrdsymb1  14539  ccatfv0  14569  lswccats1fst  14621  ccatswrd  14654  ccatpfx  14687  splfv1  14741  repswfsts  14767  cshinj  14797  swrdco  14824  cotr2g  14959  trclun  14997  resqrex  15233  sumeven  16367  ndvdsadd  16390  gcdcllem1  16477  gcdcllem3  16479  lcmftp  16610  lcmfunsnlem2lem2  16613  lcmfunsnlem2  16614  lcmfun  16619  coprmprod  16635  coprmproddvdslem  16636  divgcdcoprmex  16640  1idssfct  16654  prmodvdslcmf  17019  cshwrepswhash1  17075  xpsfrnel2  17549  xpsff1o  17552  catcone0  17670  initoeu2  18008  clatlem  18497  clatlubcl2  18499  clatglbcl2  18501  xpsmnd  18737  xpsgrp  19023  mulgfval  19033  gsmsymgrfix  19395  pmtr3ncom  19442  gsumcom3fi  19946  dprdfeq0  19991  gsumdixp  20267  lspcl  20872  lindfind  21767  lindsind  21768  lindsind2  21770  lindff1  21771  f1linds  21776  evls1maplmhm  22321  mat1dimscm  22421  mdetunilem7  22564  fvmptnn04if  22795  tgcl  22916  elcls  23021  opnnei  23068  neiptopnei  23080  cnpnei  23212  cmpfii  23357  txcnp  23568  xpstps  23758  fbun  23788  isfild  23806  snfil  23812  filconn  23831  isufil2  23856  hauspwpwf1  23935  cnextcn  24015  ustfilxp  24161  ustuqtop4  24193  xpsxms  24487  xpsms  24488  rlmnvc  24664  nmoid  24703  xrsmopn  24772  xrhmeo  24915  cphsqrtcl  25156  iscmet3  25265  iundisj  25521  ioorinv  25549  bddiblnc  25815  dvtaylp  26350  logbid1  26745  logbchbase  26748  relogbcxpb  26764  logbmpt  26765  logbfval  26767  musum  27168  lgsmodeq  27320  lgsmulsqcoprm  27321  2lgs  27385  2sqnn0  27416  pntlem3  27587  sltval2  27635  noxp1o  27642  conway  27778  scutbdaylt  27797  nbupgrel  29230  nbusgrvtxm1  29264  nb3gr2nb  29269  pthdivtx  29615  pthdlem2lem  29653  crctisclwlk  29680  wwlks  29718  wwlksonvtx  29738  wspthnonp  29742  wlkiswwlks2lem1  29752  wwlksnndef  29788  wwlksnfi  29789  clwlkclwwlkf1lem3  29888  clwlkclwwlkf1  29892  clwwlknnn  29915  clwwlkel  29928  clwwlkf1  29931  wwlksext2clwwlk  29939  clwwlknonwwlknonb  29988  umgr3v3e3cycl  30066  frgrncvvdeq  30191  sspval  30605  blo3i  30684  ajfval  30691  spanval  31215  cmcmlem  31473  leopnmid  32020  csmdsymi  32216  chirredlem4  32275  sumdmdlem  32300  iundisjf  32458  padct  32583  iundisjfi  32646  nn0difffzod  32656  hashxpe  32659  fprodex01  32673  xrpxdivcld  32743  fldgensdrg  33100  lsmsnorb  33203  mxidlnzr  33279  zringfrac  33366  extdgval  33474  ccfldextdgrr  33488  ply1annprmidl  33506  pnfneige0  33680  rrhre  33750  esumcocn  33827  hasheuni  33832  sgon  33871  sigapildsys  33909  ddemeas  33983  dya2iocct  34028  dya2iocnrect  34029  eulerpartgbij  34120  eulerpartlemgs2  34128  coinflippv  34231  signstfvneq0  34332  hgt750lemb  34416  bnj1136  34756  bnj1175  34763  bnj1408  34795  fnrelpredd  34840  pthhashvtx  34865  spthcycl  34867  upgracycumgr  34891  umgracycusgr  34892  cvmsdisj  35008  mrsubvrs  35260  mppspstlem  35309  problem4  35400  climuzcnv  35403  currybi  35416  dfon2lem7  35513  imageval  35654  filnetlem2  35991  df3nandALT1  36011  lukshef-ax2  36027  arg-ax  36028  bj-andnotim  36193  bj-modalbe  36293  bj-hbs1  36417  bj-hbsb2av  36419  bj-2uplex  36629  mptsnunlem  36945  onsucuni3  36974  fvineqsneq  37019  finixpnum  37206  fin2solem  37207  matunitlindflem2  37218  poimirlem6  37227  poimirlem7  37228  poimirlem8  37229  poimirlem18  37239  poimirlem21  37242  poimirlem22  37243  poimirlem32  37253  mblfinlem3  37260  itg2addnclem2  37273  itg2addnc  37275  ftc1anclem6  37299  heiborlem3  37414  ismndo2  37475  rngomndo  37536  isfld2  37606  isfldidl  37669  dmncan2  37678  oprabbi  37762  opabbi  37766  ac6s3f  37772  relcnveq3  37920  elrelscnveq3  38090  lsat0cv  38632  pclfinclN  39550  docavalN  40723  djavalN  40735  dochval  40951  djhval  40998  dochexmidlem8  41067  dochkr1  41078  dochkr1OLDN  41079  hdmap1fval  41396  lcmineqlem13  41641  selvcllem5  41947  mhpind  41959  pellexlem5  42392  rmyabs  42518  jm2.24  42523  islssfgi  42635  pwslnm  42657  dgraaub  42711  omlimcl2  42809  onexoegt  42811  rp-oelim2  42876  oeord2lim  42877  oeord2i  42878  ensucne0OLD  43099  iscard5  43105  clrellem  43191  frege114d  43327  frege55lem1a  43435  frege70  43502  gneispace  43703  ismnushort  43877  3impexpbicom  44057  ee3bir  44081  vk15.4j  44106  onfrALTlem2  44124  ax6e2nd  44136  dfvd1impr  44154  dfvd2impr  44182  e1bir  44208  e2bir  44211  e3bir  44317  suctrALT  44404  19.21a3con13vVD  44430  3impexpbicomVD  44435  tratrbVD  44439  ssralv2VD  44444  truniALTVD  44456  trintALTVD  44458  undif3VD  44460  csbingVD  44462  onfrALTlem3VD  44465  onfrALTlem2VD  44467  onfrALTVD  44469  csbsngVD  44471  csbxpgVD  44472  csbrngVD  44474  csbunigVD  44476  csbfv12gALTVD  44477  relopabVD  44479  ax6e2ndVD  44486  2uasbanhVD  44489  vk15.4jVD  44492  sspwimp  44496  sspwimpVD  44497  sspwimpcf  44498  sspwimpcfVD  44499  suctrALTcf  44500  suctrALTcfVD  44501  suctrALT3  44502  sspwimpALT  44503  unisnALT  44504  ax6e2ndALT  44508  isosctrlem1ALT  44512  iunconnlem2  44513  supminfxrrnmpt  44988  limsuppnflem  45233  limsupubuz  45236  cncfuni  45409  iblcncfioo  45501  stoweidlem14  45537  stoweidlem17  45540  stoweidlem35  45558  stoweidlem57  45580  stirlinglem7  45603  stirlinglem10  45606  fourierdlem54  45683  fourierdlem62  45691  fourierdlem63  45692  fourierdlem65  45694  fourierdlem73  45702  fourierdlem80  45709  fourierdlem82  45711  fourierdlem101  45730  etransclem32  45789  ioorrnopnxr  45830  subsaliuncl  45881  meadjiunlem  45988  ismeannd  45990  voliunsge0lem  45995  volmea  45997  caratheodory  46051  ovnsubaddlem2  46094  hoidmvlelem5  46122  hoiqssbllem2  46146  iinhoiicc  46197  aibandbiaiaiffb  46412  funressnvmo  46562  dfdfat2  46643  afvres  46687  tz6.12-afv  46688  ndmaovass  46721  afv2res  46754  tz6.12-afv2  46755  el1fzopredsuc  46840  fundcmpsurinjimaid  46885  iccpartiltu  46896  iccelpart  46907  lswn0  46918  ichnfimlem  46937  prprelb  46990  evenprm2  47188  dfnbgr6  47326  dfsclnbgr6  47327  lincext1  47705  sepfsepc  48129  isclatd  48177  intubeu  48178  unilbeu  48179  fullthinc  48235  setc2othin  48245