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  3497  eueq2  3678  ralun  4157  ssunieq  4903  ax6vsep  5253  opelxpi  5668  ordunidif  6370  unizlim  6445  dffo2  6758  dff1o2  6787  resdif  6803  f1o00  6817  fvimacnvALT  7011  fvcofneq  7047  exfo  7059  ressnop0  7107  fsnunfv  7143  2f1fvneq  7217  ovid  7510  ovidig  7511  dfwe2  7730  dford5  7740  onminex  7758  nnsuc  7840  1stnpr  7951  2ndnpr  7952  f1stres  7971  f2ndres  7972  1st2val  7975  2nd2val  7976  frxp  8082  soxp  8085  frxp2  8100  fprlem1  8256  tz7.49  8390  elixpsn  8887  domdifsn  9001  domunsncan  9018  unfi  9112  cnvfi  9117  fineqvlem  9185  unblem4  9218  ordiso2  9444  zfreg  9524  inf3lem3  9559  trcl  9657  unir1  9742  ssrankr1  9764  djuunxp  9850  pm54.43lem  9929  infxpenlem  9942  ween  9964  acni3  9976  kmlem1  10080  infdif  10137  ackbij1lem1  10148  fin23lem32  10273  isfin1-3  10315  axdc3lem2  10380  ac6c4  10410  zornn0g  10434  axdclem2  10449  rnct  10454  brdom3  10457  brdom5  10458  brdom4  10459  brdom6disj  10461  konigthlem  10497  pwcfsdom  10512  cfpwsdom  10513  alephom  10514  gruina  10747  grur1  10749  grothomex  10758  grothac  10759  nqpr  10943  axcnre  11093  axpre-sup  11098  ssxr  11219  le2tri3i  11280  muldivdir  11851  0nn0  12433  uzind4  12841  rpnnen1lem5  12916  elfz4  13454  eluzfz  13456  ssfzo12bi  13698  fzoopth  13699  hashgt0elex  14342  hashgt23el  14365  hashxplem  14374  hashfun  14378  ishashinf  14404  wrdsymb1  14494  ccatfv0  14524  lswccats1fst  14576  ccatswrd  14609  ccatpfx  14642  splfv1  14696  repswfsts  14722  cshinj  14752  swrdco  14779  cotr2g  14918  trclun  14956  resqrex  15192  sumeven  16333  ndvdsadd  16356  gcdcllem1  16445  gcdcllem3  16447  lcmftp  16582  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfun  16591  coprmprod  16607  coprmproddvdslem  16608  divgcdcoprmex  16612  1idssfct  16626  prmodvdslcmf  16994  cshwrepswhash1  17049  xpsfrnel2  17503  xpsff1o  17506  catcone0  17624  initoeu2  17954  clatlem  18437  clatlubcl2  18439  clatglbcl2  18441  xpsmnd  18680  xpsgrp  18967  mulgfval  18977  gsmsymgrfix  19334  pmtr3ncom  19381  gsumcom3fi  19885  dprdfeq0  19930  gsumdixp  20204  lspcl  20858  lindfind  21701  lindsind  21702  lindsind2  21704  lindff1  21705  f1linds  21710  evls1maplmhm  22240  mat1dimscm  22338  mdetunilem7  22481  fvmptnn04if  22712  tgcl  22832  elcls  22936  opnnei  22983  neiptopnei  22995  cnpnei  23127  cmpfii  23272  txcnp  23483  xpstps  23673  fbun  23703  isfild  23721  snfil  23727  filconn  23746  isufil2  23771  hauspwpwf1  23850  cnextcn  23930  ustfilxp  24076  ustuqtop4  24108  xpsxms  24398  xpsms  24399  rlmnvc  24567  nmoid  24606  xrsmopn  24677  xrhmeo  24820  cphsqrtcl  25060  iscmet3  25169  iundisj  25425  ioorinv  25453  bddiblnc  25719  dvtaylp  26254  logbid1  26654  logbchbase  26657  relogbcxpb  26673  logbmpt  26674  logbfval  26676  musum  27077  lgsmodeq  27229  lgsmulsqcoprm  27230  2lgs  27294  2sqnn0  27325  pntlem3  27496  sltval2  27544  noxp1o  27551  conway  27687  scutbdaylt  27706  nbupgrel  29248  nbusgrvtxm1  29282  nb3gr2nb  29287  pthdivtx  29630  pthdlem2lem  29670  crctisclwlk  29697  wwlks  29738  wwlksonvtx  29758  wspthnonp  29762  wlkiswwlks2lem1  29772  wwlksnndef  29808  wwlksnfi  29809  clwlkclwwlkf1lem3  29908  clwlkclwwlkf1  29912  clwwlknnn  29935  clwwlkel  29948  clwwlkf1  29951  wwlksext2clwwlk  29959  clwwlknonwwlknonb  30008  umgr3v3e3cycl  30086  frgrncvvdeq  30211  sspval  30625  blo3i  30704  ajfval  30711  spanval  31235  cmcmlem  31493  leopnmid  32040  csmdsymi  32236  chirredlem4  32295  sumdmdlem  32320  iundisjf  32491  padct  32616  iundisjfi  32692  nn0difffzod  32702  hashxpe  32705  fprodex01  32723  xrpxdivcld  32828  gsumfs2d  32968  fldgensdrg  33237  lsmsnorb  33335  mxidlnzr  33411  zringfrac  33498  lactlmhm  33603  extdgval  33622  ccfldextdgrr  33640  ply1annprmidl  33670  pnfneige0  33914  rrhre  33984  esumcocn  34043  hasheuni  34048  sgon  34087  sigapildsys  34125  ddemeas  34199  dya2iocct  34244  dya2iocnrect  34245  eulerpartgbij  34336  eulerpartlemgs2  34344  coinflippv  34448  signstfvneq0  34536  hgt750lemb  34620  bnj1136  34960  bnj1175  34967  bnj1408  34999  fnrelpredd  35052  onvf1od  35067  vonf1owev  35068  pthhashvtx  35088  spthcycl  35089  upgracycumgr  35113  umgracycusgr  35114  cvmsdisj  35230  mrsubvrs  35482  mppspstlem  35531  problem4  35628  climuzcnv  35631  currybi  35648  dfon2lem7  35750  imageval  35891  filnetlem2  36340  df3nandALT1  36360  lukshef-ax2  36376  arg-ax  36377  weiunpo  36426  bj-andnotim  36549  bj-modalbe  36649  bj-hbs1  36773  bj-hbsb2av  36775  bj-2uplex  36983  mptsnunlem  37299  onsucuni3  37328  fvineqsneq  37373  finixpnum  37572  fin2solem  37573  matunitlindflem2  37584  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  poimirlem32  37619  mblfinlem3  37626  itg2addnclem2  37639  itg2addnc  37641  ftc1anclem6  37665  heiborlem3  37780  ismndo2  37841  rngomndo  37902  isfld2  37972  isfldidl  38035  dmncan2  38044  oprabbi  38128  opabbi  38132  ac6s3f  38138  relcnveq3  38282  elrelscnveq3  38455  lsat0cv  38999  pclfinclN  39917  docavalN  41090  djavalN  41102  dochval  41318  djhval  41365  dochexmidlem8  41434  dochkr1  41445  dochkr1OLDN  41446  hdmap1fval  41763  lcmineqlem13  42002  unitscyglem4  42159  fiabv  42497  selvcllem5  42543  mhpind  42555  pellexlem5  42794  rmyabs  42920  jm2.24  42925  islssfgi  43034  pwslnm  43056  dgraaub  43110  omlimcl2  43204  onexoegt  43206  rp-oelim2  43270  oeord2lim  43271  oeord2i  43272  ensucne0OLD  43492  iscard5  43498  clrellem  43584  frege114d  43720  frege55lem1a  43828  frege70  43895  gneispace  44096  ismnushort  44263  3impexpbicom  44443  ee3bir  44466  vk15.4j  44491  onfrALTlem2  44509  ax6e2nd  44521  dfvd1impr  44539  dfvd2impr  44567  e1bir  44593  e2bir  44596  e3bir  44701  suctrALT  44788  19.21a3con13vVD  44814  3impexpbicomVD  44819  tratrbVD  44823  ssralv2VD  44828  truniALTVD  44840  trintALTVD  44842  undif3VD  44844  csbingVD  44846  onfrALTlem3VD  44849  onfrALTlem2VD  44851  onfrALTVD  44853  csbsngVD  44855  csbxpgVD  44856  csbrngVD  44858  csbunigVD  44860  csbfv12gALTVD  44861  relopabVD  44863  ax6e2ndVD  44870  2uasbanhVD  44873  vk15.4jVD  44876  sspwimp  44880  sspwimpVD  44881  sspwimpcf  44882  sspwimpcfVD  44883  suctrALTcf  44884  suctrALTcfVD  44885  suctrALT3  44886  sspwimpALT  44887  unisnALT  44888  ax6e2ndALT  44892  isosctrlem1ALT  44896  iunconnlem2  44897  prclaxpr  44948  wfaxrep  44957  supminfxrrnmpt  45440  limsuppnflem  45681  limsupubuz  45684  cncfuni  45857  iblcncfioo  45949  stoweidlem14  45985  stoweidlem17  45988  stoweidlem35  46006  stoweidlem57  46028  stirlinglem7  46051  stirlinglem10  46054  fourierdlem54  46131  fourierdlem62  46139  fourierdlem63  46140  fourierdlem65  46142  fourierdlem73  46150  fourierdlem80  46157  fourierdlem82  46159  fourierdlem101  46178  etransclem32  46237  ioorrnopnxr  46278  subsaliuncl  46329  meadjiunlem  46436  ismeannd  46438  voliunsge0lem  46443  volmea  46445  caratheodory  46499  ovnsubaddlem2  46542  hoidmvlelem5  46570  hoiqssbllem2  46594  iinhoiicc  46645  aibandbiaiaiffb  46869  funressnvmo  47019  dfdfat2  47102  afvres  47146  tz6.12-afv  47147  ndmaovass  47180  afv2res  47213  tz6.12-afv2  47214  el1fzopredsuc  47299  zp1modne  47320  fundcmpsurinjimaid  47385  iccpartiltu  47396  iccelpart  47407  lswn0  47418  ichnfimlem  47437  prprelb  47490  evenprm2  47688  dfnbgr6  47830  dfsclnbgr6  47831  isgrtri  47915  lincext1  48416  resinsnALT  48834  tposideq  48849  sepfsepc  48889  isclatd  48944  intubeu  48945  unilbeu  48946  uprcl2  49151  functhincfun  49411  fullthinc  49412  setc2othin  49428