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  1434  syl3an2br  1435  syl3an3br  1436  had1OLD  1635  nic-axALT  1707  speimfw  1998  sbbii  2115  mo4  2594  r19.30  3133  eueq2  3671  ralun  4199  ssunieq  4909  replem  5247  ax6vsep  5263  opelxpi  5695  elrelb  5784  idresdmsscocnv1  6281  ordunidif  6439  unizlim  6513  dffo2  6830  dff1o2  6860  resdif  6876  fvimacnvALT  7087  fvcofneq  7125  exfo  7137  ressnop0  7189  fsnunfv  7223  2f1fvneq  7295  ovid  7593  ovidig  7594  uniex2  7786  dfwe2  7820  dford5  7832  onminex  7850  nnsuc  7929  1stnpr  8039  2ndnpr  8040  1st2val  8063  2nd2val  8064  frxp  8175  soxp  8178  fprlem1  8356  tz7.49  8493  domdifsn  9117  domunsncan  9134  unfi  9224  cnvfi  9229  fineqvlem  9295  fissorduni  9320  unblem4  9325  zfreg  9627  elirrvOLD  9629  inf3lem3  9668  unir1  9858  ssrankr1  9884  hfsn  9957  djuunxp  10039  pm54.43lem  10120  infxpenlem  10131  ween  10153  acni3  10165  kmlem1  10268  infdif  10325  ackbij1lem1  10336  fin23lem32  10461  isfin1-3  10503  axdc3lem2  10568  ac6c4  10598  zornn0g  10622  axdclem2  10637  rnct  10643  brdom3  10646  brdom5  10647  brdom4  10648  brdom6disj  10650  konigthlem  10692  pwcfsdom  10707  cfpwsdom  10708  alephom  10709  gruina  10942  grur1  10944  grothac  10954  nqpr  11138  axcnre  11288  ssxr  11418  le2tri3i  11479  muldivdir  12049  0nn0  12661  uzind4  13073  rpnnen1lem5  13149  elfz4  13689  eluzfz  13691  ssfzo12bi  13936  fzoopth  13937  hashgt0elex  14586  hashgt23el  14610  hashxplem  14619  hashfun  14623  ishashinf  14649  wrdsymb1  14739  ccatfv0  14770  lswccats1fst  14825  ccatswrd  14860  ccatpfx  14892  splfv1  14946  cshinj  15004  swrdco  15030  cotr2g  15172  trclun  15210  resqrex  15460  sumeven  16601  ndvdsadd  16624  gcdcllem1  16713  gcdcllem3  16715  lcmftp  16855  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  divgcdcoprmex  16885  1idssfct  16899  prmodvdslcmf  17269  cshwrepswhash1  17324  xpsfrnel2  17786  xpsff1o  17789  catcone0  17911  initoeu2  18241  chnccat  18850  xpsmnd  19021  xpsgrp  19319  mulgfval  19329  gsmsymgrfix  19693  pmtr3ncom  19740  dprdfeq0  20289  gsumdixp  20599  lspcl  21302  lindsind2  22180  lindff1  22181  f1linds  22186  selvcllem5  22503  evls1maplmhm  22750  mat1dimscm  22845  matunitlindflem2  23050  tgcl  23342  elcls  23446  neiptopnei  23505  cmpfii  23782  txcnp  23994  xpstps  24184  fbun  24214  snfil  24238  filconn  24257  isufil2  24282  hauspwpwf1  24361  cnextcn  24441  ustfilxp  24587  ustuqtop4  24618  xpsxms  24908  xpsms  24909  rlmnvc  25077  nmoid  25116  xrsmopn  25187  xrhmeo  25322  cphsqrtcl  25560  iscmet3  25669  iundisj  25924  ioorinv  25952  bddiblnc  26217  dvtaylp  26754  logbid1  27153  logbchbase  27156  relogbcxpb  27172  logbmpt  27173  musum  27575  lgsmodeq  27726  lgsmulsqcoprm  27727  2lgs  27791  2sqnn0  27822  pntlem3  27993  ltsval2  28070  noxp1o  28077  cutbdaylt  28241  zsoring  28852  nb3gr2nb  30022  pthdivtx  30369  pthhashvtx  30372  pthdlem2lem  30410  crctisclwlk  30438  spthcycl  30449  wwlks  30481  wwlksonvtx  30501  wlkiswwlks2lem1  30515  wwlksnndef  30551  wwlksnfi  30552  clwlkclwwlkf1lem3  30654  clwlkclwwlkf1  30658  clwwlknnn  30681  clwwlkel  30694  wwlksext2clwwlk  30705  clwwlknonwwlknonb  30754  umgr3v3e3cycl  30842  frgrncvvdeq  30967  sspval  31382  blo3i  31461  ajfval  31468  spanval  31992  cmcmlem  32250  leopnmid  32797  csmdsymi  32993  chirredlem4  33052  sumdmdlem  33077  iundisjf  33281  iundisjfi  33484  nn0difffzod  33492  hashxpe  33495  xrpxdivcld  33597  gsumfs2d  33721  fldgensdrg  33980  lsmsnorb  34050  mxidlnzr  34096  zringfrac  34189  lactlmhm  34377  extdgval  34396  ccfldextdgrr  34415  ply1annprmidl  34450  pnfneige0  34694  rrhre  34764  esumcocn  34823  hasheuni  34828  sgon  34867  ddemeas  34980  dya2iocct  35023  dya2iocnrect  35024  eulerpartgbij  35115  eulerpartlemgs2  35123  coinflippv  35227  signstfvneq0  35312  hgt750lemb  35396  bnj1136  35738  bnj1175  35745  bnj1408  35777  fnrelpredd  35845  dfscott3  35868  fineqvnttrclselem1  35930  fineqvnttrclse  35933  unir1regs  35944  axpowg2  35956  axpowg3  35957  j0ltaleph  36049  onvf1od  36076  vonf1wev  36077  vonf1owevOLD  36079  upgracycumgr  36116  umgracycusgr  36117  cvmsdisj  36243  mrsubvrs  36495  mppspstlem  36544  problem4  36641  climuzcnv  36644  currybi  36661  dfon2lem7  36766  imageval  36907  filnetlem2  37382  lukshef-ax2  37418  arg-ax  37419  weiunpo  37468  axtco  37474  dfttc4lem2  37532  regsfromunir1  37543  bj-andnotim  37673  bj-modalbe  37805  bj-hbs1  37939  bj-hbsb2av  37941  bj-2uplex  38150  bj-axseprep  38260  mptsnunlem  38529  onsucuni3  38558  finixpnum  38796  fin2solem  38797  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem32  38838  mblfinlem3  38845  itg2addnclem2  38858  itg2addnc  38860  negprop  38911  heiborlem3  39013  ismndo2  39074  rngomndo  39135  isfld2  39205  isfldidl  39268  dmncan2  39277  oprabbi  39359  opabbi  39363  ac6s3f  39369  relcnveq3  39525  elrelscnveq3  39825  lsat0cv  40356  djavalN  42458  djhval  42721  dochkr1  42801  dochkr1OLDN  42802  hdmap1fval  43119  lcmineqlem13  43357  fiabv  43866  mhpind  43888  pellexlem5  44106  rmyabs  44231  jm2.24  44236  islssfgi  44340  pwslnm  44362  omlimcl2  44505  onexoegt  44507  rp-oelim2  44571  oeord2lim  44572  oeord2i  44573  ensucne0OLD  44792  iscard5  44798  clrellem  44883  frege114d  45019  frege55lem1a  45127  frege70  45194  gneispace  45395  ismnushort  45546  3impexpbicom  45723  ee3bir  45746  vk15.4j  45771  onfrALTlem2  45789  ax6e2nd  45801  dfvd1impr  45819  dfvd2impr  45847  e1bir  45873  e2bir  45876  e3bir  45981  suctrALT  46068  19.21a3con13vVD  46094  3impexpbicomVD  46099  tratrbVD  46103  ssralv2VD  46108  truniALTVD  46120  trintALTVD  46122  undif3VD  46124  csbingVD  46126  onfrALTlem3VD  46129  onfrALTlem2VD  46131  onfrALTVD  46133  csbsngVD  46135  csbxpgVD  46136  csbrngVD  46138  csbunigVD  46140  csbfv12gALTVD  46141  relopabVD  46143  ax6e2ndVD  46150  2uasbanhVD  46153  vk15.4jVD  46156  sspwimp  46160  sspwimpVD  46161  sspwimpcf  46162  sspwimpcfVD  46163  suctrALTcf  46164  suctrALTcfVD  46165  suctrALT3  46166  sspwimpALT  46167  unisnALT  46168  ax6e2ndALT  46172  isosctrlem1ALT  46176  iunconnlem2  46177  prclaxpr  46239  wfaxrep  46248  supminfxrrnmpt  46754  limsuppnflem  46993  limsupubuz  46996  cncfuni  47169  stoweidlem14  47297  stoweidlem35  47318  stoweidlem57  47340  stirlinglem7  47363  fourierdlem54  47443  etransclem32  47549  subsaliuncl  47641  meadjiunlem  47748  volmea  47757  caratheodory  47811  ovnsubaddlem2  47854  hoidmvlelem5  47882  hoiqssbllem2  47906  aibandbiaiaiffb  48238  funressnvmo  48388  dfdfat2  48471  afvres  48515  ndmaovass  48549  afv2res  48582  tz6.12-afv2  48583  el1fzopredsuc  48669  fundcmpsurinjimaid  48766  iccelpart  48788  lswn0  48799  ichnfimlem  48818  prprelb  48871  indprmfz  48988  evenprm2  49085  dfnbgr6  49228  dfsclnbgr6  49229  isgrtri  49314  grlimedgclnbgr  49366  idomcanr  49776  lincext1  49897  resinsnALT  50317  tposideq  50332  sepfsepc  50373  isclatd  50428  uprcl2  50636  functhincfun  50915  fullthinc  50916  setc2othin  50932  alsralrex  51336