Theorem biimpri 231

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 223. (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 227	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 219	1 ⊢ (𝜓 → 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mpbir  234  sylibr  237  sylbir  238  sylbbr  239  sylbb1  240  sylbb2  241  biimtrrid  246  imbitrrdi  255  mtbi  325  sylnib  331  simplbi2  506  biranri  511  bilanri  512  sylanbr  594  sylan2br  607  pm2.54  866  orbi2i  926  pm2.31  936  pm2.85  946  pm3.11  1008  syl3an1br  1433  syl3an2br  1434  syl3an3br  1435  had1OLD  1635  nic-axALT  1707  speimfw  1996  sbbii  2113  mo4  2592  r19.30  3130  eueq2  3668  ralun  4144  ssunieq  4904  replem  5241  ax6vsep  5257  opelxpi  5688  elrelb  5775  ordunidif  6412  unizlim  6486  dffo2  6798  dff1o2  6828  resdif  6844  fvimacnvALT  7054  fvcofneq  7091  exfo  7103  ressnop0  7155  fsnunfv  7190  2f1fvneq  7262  ovid  7559  ovidig  7560  uniex2  7752  dfwe2  7786  dford5  7796  onminex  7814  nnsuc  7893  1stnpr  8003  2ndnpr  8004  1st2val  8027  2nd2val  8028  frxp  8136  soxp  8139  fprlem1  8311  tz7.49  8448  domdifsn  9072  domunsncan  9089  unfi  9179  cnvfi  9184  fineqvlem  9250  fissorduni  9275  unblem4  9280  zfreg  9583  elirrvOLD  9585  inf3lem3  9624  unir1  9814  ssrankr1  9840  hfsn  9913  djuunxp  9995  pm54.43lem  10074  infxpenlem  10085  ween  10107  acni3  10119  kmlem1  10222  infdif  10279  ackbij1lem1  10290  fin23lem32  10415  isfin1-3  10457  axdc3lem2  10522  ac6c4  10552  zornn0g  10576  axdclem2  10591  rnct  10597  brdom3  10600  brdom5  10601  brdom4  10602  brdom6disj  10604  konigthlem  10646  pwcfsdom  10661  cfpwsdom  10662  alephom  10663  gruina  10896  grur1  10898  grothac  10908  nqpr  11092  axcnre  11242  ssxr  11372  le2tri3i  11433  muldivdir  12002  0nn0  12614  uzind4  13026  rpnnen1lem5  13102  elfz4  13642  eluzfz  13644  ssfzo12bi  13889  fzoopth  13890  hashgt0elex  14538  hashgt23el  14562  hashxplem  14571  hashfun  14575  ishashinf  14601  wrdsymb1  14691  ccatfv0  14722  lswccats1fst  14776  ccatswrd  14811  ccatpfx  14843  splfv1  14897  cshinj  14955  swrdco  14981  cotr2g  15122  trclun  15160  resqrex  15410  sumeven  16550  ndvdsadd  16573  gcdcllem1  16662  gcdcllem3  16664  lcmftp  16804  lcmfunsnlem2lem2  16807  lcmfunsnlem2  16808  divgcdcoprmex  16834  1idssfct  16848  prmodvdslcmf  17218  cshwrepswhash1  17273  xpsfrnel2  17729  xpsff1o  17732  catcone0  17854  initoeu2  18184  chnccat  18793  xpsmnd  18964  xpsgrp  19262  mulgfval  19272  gsmsymgrfix  19635  pmtr3ncom  19682  dprdfeq0  20231  gsumdixp  20541  lspcl  21244  lindsind2  22118  lindff1  22119  f1linds  22124  selvcllem5  22441  evls1maplmhm  22688  mat1dimscm  22783  matunitlindflem2  22988  tgcl  23280  elcls  23384  neiptopnei  23443  cmpfii  23720  txcnp  23932  xpstps  24122  fbun  24152  snfil  24176  filconn  24195  isufil2  24220  hauspwpwf1  24299  cnextcn  24379  ustfilxp  24525  ustuqtop4  24556  xpsxms  24846  xpsms  24847  rlmnvc  25015  nmoid  25054  xrsmopn  25125  xrhmeo  25260  cphsqrtcl  25498  iscmet3  25607  iundisj  25862  ioorinv  25890  bddiblnc  26155  dvtaylp  26690  logbid1  27089  logbchbase  27092  relogbcxpb  27108  logbmpt  27109  musum  27511  lgsmodeq  27662  lgsmulsqcoprm  27663  2lgs  27727  2sqnn0  27758  pntlem3  27929  ltsval2  28006  noxp1o  28013  cutbdaylt  28177  zsoring  28788  nb3gr2nb  29958  pthdivtx  30305  pthhashvtx  30308  pthdlem2lem  30346  crctisclwlk  30374  spthcycl  30385  wwlks  30417  wwlksonvtx  30437  wlkiswwlks2lem1  30451  wwlksnndef  30487  wwlksnfi  30488  clwlkclwwlkf1lem3  30590  clwlkclwwlkf1  30594  clwwlknnn  30617  clwwlkel  30630  wwlksext2clwwlk  30641  clwwlknonwwlknonb  30690  umgr3v3e3cycl  30778  frgrncvvdeq  30903  sspval  31318  blo3i  31397  ajfval  31404  spanval  31928  cmcmlem  32186  leopnmid  32733  csmdsymi  32929  chirredlem4  32988  sumdmdlem  33013  iundisjf  33176  iundisjfi  33381  nn0difffzod  33389  hashxpe  33392  xrpxdivcld  33494  gsumfs2d  33615  fldgensdrg  33869  lsmsnorb  33939  mxidlnzr  33985  zringfrac  34079  lactlmhm  34259  extdgval  34278  ccfldextdgrr  34297  ply1annprmidl  34332  pnfneige0  34576  rrhre  34646  esumcocn  34705  hasheuni  34710  sgon  34749  ddemeas  34862  dya2iocct  34905  dya2iocnrect  34906  eulerpartgbij  34997  eulerpartlemgs2  35005  coinflippv  35109  signstfvneq0  35194  hgt750lemb  35278  bnj1136  35620  bnj1175  35627  bnj1408  35659  fnrelpredd  35709  dfscott3  35731  fineqvnttrclselem1  35772  fineqvnttrclse  35775  unir1regs  35786  axpowg2  35798  axpowg3  35799  onvf1od  35869  vonf1wev  35870  vonf1owevOLD  35872  upgracycumgr  35897  umgracycusgr  35898  cvmsdisj  36014  mrsubvrs  36266  mppspstlem  36315  problem4  36412  climuzcnv  36415  currybi  36432  dfon2lem7  36531  imageval  36672  filnetlem2  37147  lukshef-ax2  37183  arg-ax  37184  weiunpo  37233  axtco  37239  dfttc4lem2  37297  regsfromunir1  37308  bj-andnotim  37438  bj-modalbe  37570  bj-hbs1  37704  bj-hbsb2av  37706  bj-2uplex  37915  bj-axseprep  37970  mptsnunlem  38241  onsucuni3  38270  finixpnum  38508  fin2solem  38509  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  poimirlem32  38550  mblfinlem3  38557  itg2addnclem2  38570  itg2addnc  38572  negprop  38623  heiborlem3  38727  ismndo2  38788  rngomndo  38849  isfld2  38919  isfldidl  38982  dmncan2  38991  oprabbi  39073  opabbi  39077  ac6s3f  39083  relcnveq3  39239  elrelscnveq3  39539  lsat0cv  40070  djavalN  42172  djhval  42435  dochkr1  42515  dochkr1OLDN  42516  hdmap1fval  42833  lcmineqlem13  43071  fiabv  43580  mhpind  43602  pellexlem5  43819  rmyabs  43944  jm2.24  43949  islssfgi  44058  pwslnm  44080  omlimcl2  44228  onexoegt  44230  rp-oelim2  44294  oeord2lim  44295  oeord2i  44296  ensucne0OLD  44515  iscard5  44521  clrellem  44607  frege114d  44743  frege55lem1a  44851  frege70  44918  gneispace  45119  ismnushort  45270  3impexpbicom  45448  ee3bir  45471  vk15.4j  45496  onfrALTlem2  45514  ax6e2nd  45526  dfvd1impr  45544  dfvd2impr  45572  e1bir  45598  e2bir  45601  e3bir  45706  suctrALT  45793  19.21a3con13vVD  45819  3impexpbicomVD  45824  tratrbVD  45828  ssralv2VD  45833  truniALTVD  45845  trintALTVD  45847  undif3VD  45849  csbingVD  45851  onfrALTlem3VD  45854  onfrALTlem2VD  45856  onfrALTVD  45858  csbsngVD  45860  csbxpgVD  45861  csbrngVD  45863  csbunigVD  45865  csbfv12gALTVD  45866  relopabVD  45868  ax6e2ndVD  45875  2uasbanhVD  45878  vk15.4jVD  45881  sspwimp  45885  sspwimpVD  45886  sspwimpcf  45887  sspwimpcfVD  45888  suctrALTcf  45889  suctrALTcfVD  45890  suctrALT3  45891  sspwimpALT  45892  unisnALT  45893  ax6e2ndALT  45897  isosctrlem1ALT  45901  iunconnlem2  45902  prclaxpr  45953  wfaxrep  45962  supminfxrrnmpt  46450  limsuppnflem  46689  limsupubuz  46692  cncfuni  46865  stoweidlem14  46993  stoweidlem35  47014  stoweidlem57  47036  stirlinglem7  47059  fourierdlem54  47139  etransclem32  47245  subsaliuncl  47337  meadjiunlem  47444  volmea  47453  caratheodory  47507  ovnsubaddlem2  47550  hoidmvlelem5  47578  hoiqssbllem2  47602  aibandbiaiaiffb  47934  funressnvmo  48084  dfdfat2  48167  afvres  48211  ndmaovass  48245  afv2res  48278  tz6.12-afv2  48279  el1fzopredsuc  48365  fundcmpsurinjimaid  48462  iccelpart  48484  lswn0  48495  ichnfimlem  48514  prprelb  48567  indprmfz  48684  evenprm2  48781  dfnbgr6  48924  dfsclnbgr6  48925  isgrtri  49010  grlimedgclnbgr  49062  idomcanr  49414  lincext1  49535  resinsnALT  49950  tposideq  49965  sepfsepc  50005  isclatd  50060  uprcl2  50266  functhincfun  50526  fullthinc  50527  setc2othin  50543  alsralrex  50877