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  1634  nic-axALT  1706  speimfw  1995  sbbii  2112  mo4  2591  r19.30  3129  eueq2  3667  ralun  4196  ssunieq  4903  replem  5240  ax6vsep  5256  opelxpi  5687  elrelb  5774  ordunidif  6413  unizlim  6487  dffo2  6800  dff1o2  6830  resdif  6846  fvimacnvALT  7056  fvcofneq  7093  exfo  7105  ressnop0  7157  fsnunfv  7192  2f1fvneq  7264  ovid  7561  ovidig  7562  uniex2  7754  dfwe2  7788  dford5  7798  onminex  7816  nnsuc  7895  1stnpr  8005  2ndnpr  8006  1st2val  8029  2nd2val  8030  frxp  8138  soxp  8141  fprlem1  8319  tz7.49  8456  domdifsn  9080  domunsncan  9097  unfi  9187  cnvfi  9192  fineqvlem  9258  fissorduni  9283  unblem4  9288  zfreg  9591  elirrvOLD  9593  inf3lem3  9632  unir1  9822  ssrankr1  9848  hfsn  9921  djuunxp  10003  pm54.43lem  10082  infxpenlem  10093  ween  10115  acni3  10127  kmlem1  10230  infdif  10287  ackbij1lem1  10298  fin23lem32  10423  isfin1-3  10465  axdc3lem2  10530  ac6c4  10560  zornn0g  10584  axdclem2  10599  rnct  10605  brdom3  10608  brdom5  10609  brdom4  10610  brdom6disj  10612  konigthlem  10654  pwcfsdom  10669  cfpwsdom  10670  alephom  10671  gruina  10904  grur1  10906  grothac  10916  nqpr  11100  axcnre  11250  ssxr  11380  le2tri3i  11441  muldivdir  12010  0nn0  12622  uzind4  13034  rpnnen1lem5  13110  elfz4  13650  eluzfz  13652  ssfzo12bi  13897  fzoopth  13898  hashgt0elex  14546  hashgt23el  14570  hashxplem  14579  hashfun  14583  ishashinf  14609  wrdsymb1  14699  ccatfv0  14730  lswccats1fst  14784  ccatswrd  14819  ccatpfx  14851  splfv1  14905  cshinj  14963  swrdco  14989  cotr2g  15130  trclun  15168  resqrex  15418  sumeven  16558  ndvdsadd  16581  gcdcllem1  16670  gcdcllem3  16672  lcmftp  16812  lcmfunsnlem2lem2  16815  lcmfunsnlem2  16816  divgcdcoprmex  16842  1idssfct  16856  prmodvdslcmf  17226  cshwrepswhash1  17281  xpsfrnel2  17737  xpsff1o  17740  catcone0  17862  initoeu2  18192  chnccat  18801  xpsmnd  18972  xpsgrp  19270  mulgfval  19280  gsmsymgrfix  19643  pmtr3ncom  19690  dprdfeq0  20239  gsumdixp  20549  lspcl  21252  lindsind2  22126  lindff1  22127  f1linds  22132  selvcllem5  22449  evls1maplmhm  22696  mat1dimscm  22791  matunitlindflem2  22996  tgcl  23288  elcls  23392  neiptopnei  23451  cmpfii  23728  txcnp  23940  xpstps  24130  fbun  24160  snfil  24184  filconn  24203  isufil2  24228  hauspwpwf1  24307  cnextcn  24387  ustfilxp  24533  ustuqtop4  24564  xpsxms  24854  xpsms  24855  rlmnvc  25023  nmoid  25062  xrsmopn  25133  xrhmeo  25268  cphsqrtcl  25506  iscmet3  25615  iundisj  25870  ioorinv  25898  bddiblnc  26163  dvtaylp  26698  logbid1  27097  logbchbase  27100  relogbcxpb  27116  logbmpt  27117  musum  27519  lgsmodeq  27670  lgsmulsqcoprm  27671  2lgs  27735  2sqnn0  27766  pntlem3  27937  ltsval2  28014  noxp1o  28021  cutbdaylt  28185  zsoring  28796  nb3gr2nb  29966  pthdivtx  30313  pthhashvtx  30316  pthdlem2lem  30354  crctisclwlk  30382  spthcycl  30393  wwlks  30425  wwlksonvtx  30445  wlkiswwlks2lem1  30459  wwlksnndef  30495  wwlksnfi  30496  clwlkclwwlkf1lem3  30598  clwlkclwwlkf1  30602  clwwlknnn  30625  clwwlkel  30638  wwlksext2clwwlk  30649  clwwlknonwwlknonb  30698  umgr3v3e3cycl  30786  frgrncvvdeq  30911  sspval  31326  blo3i  31405  ajfval  31412  spanval  31936  cmcmlem  32194  leopnmid  32741  csmdsymi  32937  chirredlem4  32996  sumdmdlem  33021  iundisjf  33226  iundisjfi  33431  nn0difffzod  33439  hashxpe  33442  xrpxdivcld  33544  gsumfs2d  33665  fldgensdrg  33919  lsmsnorb  33989  mxidlnzr  34035  zringfrac  34129  lactlmhm  34309  extdgval  34328  ccfldextdgrr  34347  ply1annprmidl  34382  pnfneige0  34626  rrhre  34696  esumcocn  34755  hasheuni  34760  sgon  34799  ddemeas  34912  dya2iocct  34955  dya2iocnrect  34956  eulerpartgbij  35047  eulerpartlemgs2  35055  coinflippv  35159  signstfvneq0  35244  hgt750lemb  35328  bnj1136  35670  bnj1175  35677  bnj1408  35709  fnrelpredd  35763  dfscott3  35786  fineqvnttrclselem1  35832  fineqvnttrclse  35835  unir1regs  35846  axpowg2  35858  axpowg3  35859  onvf1od  35929  vonf1wev  35930  vonf1owevOLD  35932  upgracycumgr  35961  umgracycusgr  35962  cvmsdisj  36078  mrsubvrs  36330  mppspstlem  36379  problem4  36476  climuzcnv  36479  currybi  36496  dfon2lem7  36594  imageval  36735  filnetlem2  37210  lukshef-ax2  37246  arg-ax  37247  weiunpo  37296  axtco  37302  dfttc4lem2  37360  regsfromunir1  37371  bj-andnotim  37501  bj-modalbe  37633  bj-hbs1  37767  bj-hbsb2av  37769  bj-2uplex  37978  bj-axseprep  38033  mptsnunlem  38305  onsucuni3  38334  finixpnum  38572  fin2solem  38573  poimirlem6  38588  poimirlem7  38589  poimirlem8  38590  poimirlem18  38600  poimirlem21  38603  poimirlem22  38604  poimirlem32  38614  mblfinlem3  38621  itg2addnclem2  38634  itg2addnc  38636  negprop  38687  heiborlem3  38791  ismndo2  38852  rngomndo  38913  isfld2  38983  isfldidl  39046  dmncan2  39055  oprabbi  39137  opabbi  39141  ac6s3f  39147  relcnveq3  39303  elrelscnveq3  39603  lsat0cv  40134  djavalN  42236  djhval  42499  dochkr1  42579  dochkr1OLDN  42580  hdmap1fval  42897  lcmineqlem13  43135  fiabv  43644  mhpind  43666  pellexlem5  43884  rmyabs  44009  jm2.24  44014  islssfgi  44118  pwslnm  44140  omlimcl2  44288  onexoegt  44290  rp-oelim2  44354  oeord2lim  44355  oeord2i  44356  ensucne0OLD  44575  iscard5  44581  clrellem  44666  frege114d  44802  frege55lem1a  44910  frege70  44977  gneispace  45178  ismnushort  45329  3impexpbicom  45507  ee3bir  45530  vk15.4j  45555  onfrALTlem2  45573  ax6e2nd  45585  dfvd1impr  45603  dfvd2impr  45631  e1bir  45657  e2bir  45660  e3bir  45765  suctrALT  45852  19.21a3con13vVD  45878  3impexpbicomVD  45883  tratrbVD  45887  ssralv2VD  45892  truniALTVD  45904  trintALTVD  45906  undif3VD  45908  csbingVD  45910  onfrALTlem3VD  45913  onfrALTlem2VD  45915  onfrALTVD  45917  csbsngVD  45919  csbxpgVD  45920  csbrngVD  45922  csbunigVD  45924  csbfv12gALTVD  45925  relopabVD  45927  ax6e2ndVD  45934  2uasbanhVD  45937  vk15.4jVD  45940  sspwimp  45944  sspwimpVD  45945  sspwimpcf  45946  sspwimpcfVD  45947  suctrALTcf  45948  suctrALTcfVD  45949  suctrALT3  45950  sspwimpALT  45951  unisnALT  45952  ax6e2ndALT  45956  isosctrlem1ALT  45960  iunconnlem2  45961  prclaxpr  46019  wfaxrep  46028  supminfxrrnmpt  46525  limsuppnflem  46764  limsupubuz  46767  cncfuni  46940  stoweidlem14  47068  stoweidlem35  47089  stoweidlem57  47111  stirlinglem7  47134  fourierdlem54  47214  etransclem32  47320  subsaliuncl  47412  meadjiunlem  47519  volmea  47528  caratheodory  47582  ovnsubaddlem2  47625  hoidmvlelem5  47653  hoiqssbllem2  47677  aibandbiaiaiffb  48009  funressnvmo  48159  dfdfat2  48242  afvres  48286  ndmaovass  48320  afv2res  48353  tz6.12-afv2  48354  el1fzopredsuc  48440  fundcmpsurinjimaid  48537  iccelpart  48559  lswn0  48570  ichnfimlem  48589  prprelb  48642  indprmfz  48759  evenprm2  48856  dfnbgr6  48999  dfsclnbgr6  49000  isgrtri  49085  grlimedgclnbgr  49137  idomcanr  49489  lincext1  49610  resinsnALT  50025  tposideq  50040  sepfsepc  50080  isclatd  50135  uprcl2  50341  functhincfun  50601  fullthinc  50602  setc2othin  50618  alsralrex  50952