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  4195  ssunieq  4903  replem  5240  ax6vsep  5256  opelxpi  5687  elrelb  5775  ordunidif  6415  unizlim  6489  dffo2  6803  dff1o2  6833  resdif  6849  fvimacnvALT  7059  fvcofneq  7096  exfo  7108  ressnop0  7160  fsnunfv  7194  2f1fvneq  7266  ovid  7563  ovidig  7564  uniex2  7756  dfwe2  7790  dford5  7800  onminex  7818  nnsuc  7897  1stnpr  8007  2ndnpr  8008  1st2val  8031  2nd2val  8032  frxp  8142  soxp  8145  fprlem1  8323  tz7.49  8460  domdifsn  9084  domunsncan  9101  unfi  9191  cnvfi  9196  fineqvlem  9262  fissorduni  9287  unblem4  9292  zfreg  9595  elirrvOLD  9597  inf3lem3  9636  unir1  9826  ssrankr1  9852  hfsn  9925  djuunxp  10007  pm54.43lem  10086  infxpenlem  10097  ween  10119  acni3  10131  kmlem1  10234  infdif  10291  ackbij1lem1  10302  fin23lem32  10427  isfin1-3  10469  axdc3lem2  10534  ac6c4  10564  zornn0g  10588  axdclem2  10603  rnct  10609  brdom3  10612  brdom5  10613  brdom4  10614  brdom6disj  10616  konigthlem  10658  pwcfsdom  10673  cfpwsdom  10674  alephom  10675  gruina  10908  grur1  10910  grothac  10920  nqpr  11104  axcnre  11254  ssxr  11384  le2tri3i  11445  muldivdir  12014  0nn0  12626  uzind4  13038  rpnnen1lem5  13114  elfz4  13654  eluzfz  13656  ssfzo12bi  13901  fzoopth  13902  hashgt0elex  14550  hashgt23el  14574  hashxplem  14583  hashfun  14587  ishashinf  14613  wrdsymb1  14703  ccatfv0  14734  lswccats1fst  14789  ccatswrd  14824  ccatpfx  14856  splfv1  14910  cshinj  14968  swrdco  14994  cotr2g  15136  trclun  15174  resqrex  15424  sumeven  16564  ndvdsadd  16587  gcdcllem1  16676  gcdcllem3  16678  lcmftp  16818  lcmfunsnlem2lem2  16821  lcmfunsnlem2  16822  divgcdcoprmex  16848  1idssfct  16862  prmodvdslcmf  17232  cshwrepswhash1  17287  xpsfrnel2  17743  xpsff1o  17746  catcone0  17868  initoeu2  18198  chnccat  18807  xpsmnd  18978  xpsgrp  19276  mulgfval  19286  gsmsymgrfix  19649  pmtr3ncom  19696  dprdfeq0  20245  gsumdixp  20555  lspcl  21258  lindsind2  22132  lindff1  22133  f1linds  22138  selvcllem5  22455  evls1maplmhm  22702  mat1dimscm  22797  matunitlindflem2  23002  tgcl  23294  elcls  23398  neiptopnei  23457  cmpfii  23734  txcnp  23946  xpstps  24136  fbun  24166  snfil  24190  filconn  24209  isufil2  24234  hauspwpwf1  24313  cnextcn  24393  ustfilxp  24539  ustuqtop4  24570  xpsxms  24860  xpsms  24861  rlmnvc  25029  nmoid  25068  xrsmopn  25139  xrhmeo  25274  cphsqrtcl  25512  iscmet3  25621  iundisj  25876  ioorinv  25904  bddiblnc  26169  dvtaylp  26704  logbid1  27103  logbchbase  27106  relogbcxpb  27122  logbmpt  27123  musum  27525  lgsmodeq  27676  lgsmulsqcoprm  27677  2lgs  27741  2sqnn0  27772  pntlem3  27943  ltsval2  28020  noxp1o  28027  cutbdaylt  28191  zsoring  28802  nb3gr2nb  29972  pthdivtx  30319  pthhashvtx  30322  pthdlem2lem  30360  crctisclwlk  30388  spthcycl  30399  wwlks  30431  wwlksonvtx  30451  wlkiswwlks2lem1  30465  wwlksnndef  30501  wwlksnfi  30502  clwlkclwwlkf1lem3  30604  clwlkclwwlkf1  30608  clwwlknnn  30631  clwwlkel  30644  wwlksext2clwwlk  30655  clwwlknonwwlknonb  30704  umgr3v3e3cycl  30792  frgrncvvdeq  30917  sspval  31332  blo3i  31411  ajfval  31418  spanval  31942  cmcmlem  32200  leopnmid  32747  csmdsymi  32943  chirredlem4  33002  sumdmdlem  33027  iundisjf  33232  iundisjfi  33436  nn0difffzod  33444  hashxpe  33447  xrpxdivcld  33549  gsumfs2d  33670  fldgensdrg  33924  lsmsnorb  33994  mxidlnzr  34040  zringfrac  34134  lactlmhm  34314  extdgval  34333  ccfldextdgrr  34352  ply1annprmidl  34387  pnfneige0  34631  rrhre  34701  esumcocn  34760  hasheuni  34765  sgon  34804  ddemeas  34917  dya2iocct  34960  dya2iocnrect  34961  eulerpartgbij  35052  eulerpartlemgs2  35060  coinflippv  35164  signstfvneq0  35249  hgt750lemb  35333  bnj1136  35675  bnj1175  35682  bnj1408  35714  fnrelpredd  35774  dfscott3  35799  fineqvnttrclselem1  35847  fineqvnttrclse  35850  unir1regs  35861  axpowg2  35873  axpowg3  35874  j0ltaleph  35949  onvf1od  35956  vonf1wev  35957  vonf1owevOLD  35959  upgracycumgr  35996  umgracycusgr  35997  cvmsdisj  36123  mrsubvrs  36375  mppspstlem  36424  problem4  36521  climuzcnv  36524  currybi  36541  dfon2lem7  36645  imageval  36786  filnetlem2  37261  lukshef-ax2  37297  arg-ax  37298  weiunpo  37347  axtco  37353  dfttc4lem2  37411  regsfromunir1  37422  bj-andnotim  37552  bj-modalbe  37684  bj-hbs1  37818  bj-hbsb2av  37820  bj-2uplex  38029  bj-axseprep  38096  mptsnunlem  38368  onsucuni3  38397  finixpnum  38635  fin2solem  38636  poimirlem6  38651  poimirlem7  38652  poimirlem8  38653  poimirlem18  38663  poimirlem21  38666  poimirlem22  38667  poimirlem32  38677  mblfinlem3  38684  itg2addnclem2  38697  itg2addnc  38699  negprop  38750  heiborlem3  38854  ismndo2  38915  rngomndo  38976  isfld2  39046  isfldidl  39109  dmncan2  39118  oprabbi  39200  opabbi  39204  ac6s3f  39210  relcnveq3  39366  elrelscnveq3  39666  lsat0cv  40197  djavalN  42299  djhval  42562  dochkr1  42642  dochkr1OLDN  42643  hdmap1fval  42960  lcmineqlem13  43198  fiabv  43707  mhpind  43729  pellexlem5  43947  rmyabs  44072  jm2.24  44077  islssfgi  44181  pwslnm  44203  omlimcl2  44351  onexoegt  44353  rp-oelim2  44417  oeord2lim  44418  oeord2i  44419  ensucne0OLD  44638  iscard5  44644  clrellem  44729  frege114d  44865  frege55lem1a  44973  frege70  45040  gneispace  45241  ismnushort  45392  3impexpbicom  45570  ee3bir  45593  vk15.4j  45618  onfrALTlem2  45636  ax6e2nd  45648  dfvd1impr  45666  dfvd2impr  45694  e1bir  45720  e2bir  45723  e3bir  45828  suctrALT  45915  19.21a3con13vVD  45941  3impexpbicomVD  45946  tratrbVD  45950  ssralv2VD  45955  truniALTVD  45967  trintALTVD  45969  undif3VD  45971  csbingVD  45973  onfrALTlem3VD  45976  onfrALTlem2VD  45978  onfrALTVD  45980  csbsngVD  45982  csbxpgVD  45983  csbrngVD  45985  csbunigVD  45987  csbfv12gALTVD  45988  relopabVD  45990  ax6e2ndVD  45997  2uasbanhVD  46000  vk15.4jVD  46003  sspwimp  46007  sspwimpVD  46008  sspwimpcf  46009  sspwimpcfVD  46010  suctrALTcf  46011  suctrALTcfVD  46012  suctrALT3  46013  sspwimpALT  46014  unisnALT  46015  ax6e2ndALT  46019  isosctrlem1ALT  46023  iunconnlem2  46024  prclaxpr  46082  wfaxrep  46091  supminfxrrnmpt  46588  limsuppnflem  46827  limsupubuz  46830  cncfuni  47003  stoweidlem14  47131  stoweidlem35  47152  stoweidlem57  47174  stirlinglem7  47197  fourierdlem54  47277  etransclem32  47383  subsaliuncl  47475  meadjiunlem  47582  volmea  47591  caratheodory  47645  ovnsubaddlem2  47688  hoidmvlelem5  47716  hoiqssbllem2  47740  aibandbiaiaiffb  48072  funressnvmo  48222  dfdfat2  48305  afvres  48349  ndmaovass  48383  afv2res  48416  tz6.12-afv2  48417  el1fzopredsuc  48503  fundcmpsurinjimaid  48600  iccelpart  48622  lswn0  48633  ichnfimlem  48652  prprelb  48705  indprmfz  48822  evenprm2  48919  dfnbgr6  49062  dfsclnbgr6  49063  isgrtri  49148  grlimedgclnbgr  49200  idomcanr  49552  lincext1  49673  resinsnALT  50093  tposideq  50108  sepfsepc  50149  isclatd  50204  uprcl2  50412  functhincfun  50691  fullthinc  50692  setc2othin  50708  alsralrex  51090