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  17628  initoeu2  17958  clatlem  18443  clatlubcl2  18445  clatglbcl2  18447  xpsmnd  18686  xpsgrp  18973  mulgfval  18983  gsmsymgrfix  19342  pmtr3ncom  19389  gsumcom3fi  19893  dprdfeq0  19938  gsumdixp  20239  lspcl  20914  lindfind  21758  lindsind  21759  lindsind2  21761  lindff1  21762  f1linds  21767  evls1maplmhm  22297  mat1dimscm  22395  mdetunilem7  22538  fvmptnn04if  22769  tgcl  22889  elcls  22993  opnnei  23040  neiptopnei  23052  cnpnei  23184  cmpfii  23329  txcnp  23540  xpstps  23730  fbun  23760  isfild  23778  snfil  23784  filconn  23803  isufil2  23828  hauspwpwf1  23907  cnextcn  23987  ustfilxp  24133  ustuqtop4  24165  xpsxms  24455  xpsms  24456  rlmnvc  24624  nmoid  24663  xrsmopn  24734  xrhmeo  24877  cphsqrtcl  25117  iscmet3  25226  iundisj  25482  ioorinv  25510  bddiblnc  25776  dvtaylp  26311  logbid1  26711  logbchbase  26714  relogbcxpb  26730  logbmpt  26731  logbfval  26733  musum  27134  lgsmodeq  27286  lgsmulsqcoprm  27287  2lgs  27351  2sqnn0  27382  pntlem3  27553  sltval2  27601  noxp1o  27608  conway  27745  scutbdaylt  27764  zsoring  28336  nbupgrel  29325  nbusgrvtxm1  29359  nb3gr2nb  29364  pthdivtx  29707  pthdlem2lem  29747  crctisclwlk  29774  wwlks  29815  wwlksonvtx  29835  wspthnonp  29839  wlkiswwlks2lem1  29849  wwlksnndef  29885  wwlksnfi  29886  clwlkclwwlkf1lem3  29985  clwlkclwwlkf1  29989  clwwlknnn  30012  clwwlkel  30025  clwwlkf1  30028  wwlksext2clwwlk  30036  clwwlknonwwlknonb  30085  umgr3v3e3cycl  30163  frgrncvvdeq  30288  sspval  30702  blo3i  30781  ajfval  30788  spanval  31312  cmcmlem  31570  leopnmid  32117  csmdsymi  32313  chirredlem4  32372  sumdmdlem  32397  iundisjf  32568  padct  32693  iundisjfi  32769  nn0difffzod  32779  hashxpe  32782  fprodex01  32800  xrpxdivcld  32905  gsumfs2d  33038  fldgensdrg  33280  lsmsnorb  33355  mxidlnzr  33431  zringfrac  33518  lactlmhm  33623  extdgval  33642  ccfldextdgrr  33660  ply1annprmidl  33690  pnfneige0  33934  rrhre  34004  esumcocn  34063  hasheuni  34068  sgon  34107  sigapildsys  34145  ddemeas  34219  dya2iocct  34264  dya2iocnrect  34265  eulerpartgbij  34356  eulerpartlemgs2  34364  coinflippv  34468  signstfvneq0  34556  hgt750lemb  34640  bnj1136  34980  bnj1175  34987  bnj1408  35019  fnrelpredd  35072  onvf1od  35087  vonf1owev  35088  pthhashvtx  35108  spthcycl  35109  upgracycumgr  35133  umgracycusgr  35134  cvmsdisj  35250  mrsubvrs  35502  mppspstlem  35551  problem4  35648  climuzcnv  35651  currybi  35668  dfon2lem7  35770  imageval  35911  filnetlem2  36360  df3nandALT1  36380  lukshef-ax2  36396  arg-ax  36397  weiunpo  36446  bj-andnotim  36569  bj-modalbe  36669  bj-hbs1  36793  bj-hbsb2av  36795  bj-2uplex  37003  mptsnunlem  37319  onsucuni3  37348  fvineqsneq  37393  finixpnum  37592  fin2solem  37593  matunitlindflem2  37604  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem32  37639  mblfinlem3  37646  itg2addnclem2  37659  itg2addnc  37661  ftc1anclem6  37685  heiborlem3  37800  ismndo2  37861  rngomndo  37922  isfld2  37992  isfldidl  38055  dmncan2  38064  oprabbi  38148  opabbi  38152  ac6s3f  38158  relcnveq3  38302  elrelscnveq3  38475  lsat0cv  39019  pclfinclN  39937  docavalN  41110  djavalN  41122  dochval  41338  djhval  41385  dochexmidlem8  41454  dochkr1  41465  dochkr1OLDN  41466  hdmap1fval  41783  lcmineqlem13  42022  unitscyglem4  42179  fiabv  42517  selvcllem5  42563  mhpind  42575  pellexlem5  42814  rmyabs  42940  jm2.24  42945  islssfgi  43054  pwslnm  43076  dgraaub  43130  omlimcl2  43224  onexoegt  43226  rp-oelim2  43290  oeord2lim  43291  oeord2i  43292  ensucne0OLD  43512  iscard5  43518  clrellem  43604  frege114d  43740  frege55lem1a  43848  frege70  43915  gneispace  44116  ismnushort  44283  3impexpbicom  44463  ee3bir  44486  vk15.4j  44511  onfrALTlem2  44529  ax6e2nd  44541  dfvd1impr  44559  dfvd2impr  44587  e1bir  44613  e2bir  44616  e3bir  44721  suctrALT  44808  19.21a3con13vVD  44834  3impexpbicomVD  44839  tratrbVD  44843  ssralv2VD  44848  truniALTVD  44860  trintALTVD  44862  undif3VD  44864  csbingVD  44866  onfrALTlem3VD  44869  onfrALTlem2VD  44871  onfrALTVD  44873  csbsngVD  44875  csbxpgVD  44876  csbrngVD  44878  csbunigVD  44880  csbfv12gALTVD  44881  relopabVD  44883  ax6e2ndVD  44890  2uasbanhVD  44893  vk15.4jVD  44896  sspwimp  44900  sspwimpVD  44901  sspwimpcf  44902  sspwimpcfVD  44903  suctrALTcf  44904  suctrALTcfVD  44905  suctrALT3  44906  sspwimpALT  44907  unisnALT  44908  ax6e2ndALT  44912  isosctrlem1ALT  44916  iunconnlem2  44917  prclaxpr  44968  wfaxrep  44977  supminfxrrnmpt  45460  limsuppnflem  45701  limsupubuz  45704  cncfuni  45877  iblcncfioo  45969  stoweidlem14  46005  stoweidlem17  46008  stoweidlem35  46026  stoweidlem57  46048  stirlinglem7  46071  stirlinglem10  46074  fourierdlem54  46151  fourierdlem62  46159  fourierdlem63  46160  fourierdlem65  46162  fourierdlem73  46170  fourierdlem80  46177  fourierdlem82  46179  fourierdlem101  46198  etransclem32  46257  ioorrnopnxr  46298  subsaliuncl  46349  meadjiunlem  46456  ismeannd  46458  voliunsge0lem  46463  volmea  46465  caratheodory  46519  ovnsubaddlem2  46562  hoidmvlelem5  46590  hoiqssbllem2  46614  iinhoiicc  46665  aibandbiaiaiffb  46889  funressnvmo  47039  dfdfat2  47122  afvres  47166  tz6.12-afv  47167  ndmaovass  47200  afv2res  47233  tz6.12-afv2  47234  el1fzopredsuc  47319  zp1modne  47340  fundcmpsurinjimaid  47405  iccpartiltu  47416  iccelpart  47427  lswn0  47438  ichnfimlem  47457  prprelb  47510  evenprm2  47708  dfnbgr6  47850  dfsclnbgr6  47851  isgrtri  47935  lincext1  48436  resinsnALT  48854  tposideq  48869  sepfsepc  48909  isclatd  48964  intubeu  48965  unilbeu  48966  uprcl2  49171  functhincfun  49431  fullthinc  49432  setc2othin  49448