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 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  mpbir  234  sylibr  237  sylbir  238  sylbbr  239  sylbb1  240  sylbb2  241  biimtrrid  246  imbitrrdi  255  mtbi  325  sylnib  331  simplbi2  505  biranri  510  bilanri  511  sylanbr  593  sylan2br  606  pm2.54  865  orbi2i  925  pm2.31  935  pm2.85  945  pm3.11  1008  syl3an1br  1433  syl3an2br  1434  syl3an3br  1435  had1  1633  nic-axALT  1704  speimfw  1993  sbbii  2110  mo4  2594  r19.30  3132  eueq2  3673  ralun  4151  ssunieq  4909  replem  5249  ax6vsep  5266  opelxpi  5698  ordunidif  6411  unizlim  6485  dffo2  6796  dff1o2  6826  resdif  6842  fvimacnvALT  7052  fvcofneq  7088  exfo  7100  ressnop0  7150  fsnunfv  7185  2f1fvneq  7258  ovid  7551  ovidig  7552  uniex2  7735  dfwe2  7769  dford5  7779  onminex  7797  nnsuc  7876  1stnpr  7986  2ndnpr  7987  1st2val  8010  2nd2val  8011  frxp  8118  soxp  8121  fprlem1  8293  tz7.49  8428  domdifsn  9044  domunsncan  9061  unfi  9151  cnvfi  9156  fineqvlem  9222  unblem4  9251  zfreg  9554  elirrvOLD  9556  inf3lem3  9595  unir1  9781  ssrankr1  9803  djuunxp  9903  pm54.43lem  9982  infxpenlem  9993  ween  10015  acni3  10027  kmlem1  10130  infdif  10187  ackbij1lem1  10198  fin23lem32  10323  isfin1-3  10365  axdc3lem2  10430  ac6c4  10460  zornn0g  10484  axdclem2  10499  rnct  10504  brdom3  10507  brdom5  10508  brdom4  10509  brdom6disj  10511  konigthlem  10548  pwcfsdom  10563  cfpwsdom  10564  alephom  10565  gruina  10798  grur1  10800  grothac  10810  nqpr  10994  axcnre  11144  ssxr  11274  le2tri3i  11335  muldivdir  11902  0nn0  12514  uzind4  12925  rpnnen1lem5  13000  elfz4  13540  eluzfz  13542  ssfzo12bi  13786  fzoopth  13787  hashgt0elex  14433  hashgt23el  14457  hashxplem  14466  hashfun  14470  ishashinf  14496  wrdsymb1  14586  ccatfv0  14617  lswccats1fst  14669  ccatswrd  14702  ccatpfx  14734  splfv1  14788  cshinj  14844  swrdco  14870  cotr2g  15009  trclun  15047  resqrex  15297  sumeven  16440  ndvdsadd  16463  gcdcllem1  16552  gcdcllem3  16554  lcmftp  16689  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  divgcdcoprmex  16719  1idssfct  16733  prmodvdslcmf  17102  cshwrepswhash1  17157  xpsfrnel2  17613  xpsff1o  17616  catcone0  17738  initoeu2  18068  chnccat  18677  xpsmnd  18830  xpsgrp  19120  mulgfval  19130  gsmsymgrfix  19493  pmtr3ncom  19540  dprdfeq0  20089  gsumdixp  20396  lspcl  21097  lindsind2  21969  lindff1  21970  f1linds  21975  selvcllem5  22290  evls1maplmhm  22537  mat1dimscm  22632  tgcl  23126  elcls  23230  neiptopnei  23289  cmpfii  23566  txcnp  23777  xpstps  23967  fbun  23997  snfil  24021  filconn  24040  isufil2  24065  hauspwpwf1  24144  cnextcn  24224  ustfilxp  24370  ustuqtop4  24401  xpsxms  24691  xpsms  24692  rlmnvc  24860  nmoid  24899  xrsmopn  24970  xrhmeo  25105  cphsqrtcl  25343  iscmet3  25452  iundisj  25707  ioorinv  25735  bddiblnc  26001  dvtaylp  26533  logbid1  26933  logbchbase  26936  relogbcxpb  26952  logbmpt  26953  musum  27355  lgsmodeq  27506  lgsmulsqcoprm  27507  2lgs  27571  2sqnn0  27602  pntlem3  27773  ltsval2  27820  noxp1o  27827  cutbdaylt  27991  zsoring  28602  nb3gr2nb  29734  pthdivtx  30076  pthdlem2lem  30116  crctisclwlk  30143  wwlks  30184  wwlksonvtx  30204  wlkiswwlks2lem1  30218  wwlksnndef  30254  wwlksnfi  30255  clwlkclwwlkf1lem3  30357  clwlkclwwlkf1  30361  clwwlknnn  30384  clwwlkel  30397  wwlksext2clwwlk  30408  clwwlknonwwlknonb  30457  umgr3v3e3cycl  30535  frgrncvvdeq  30660  sspval  31075  blo3i  31154  ajfval  31161  spanval  31685  cmcmlem  31943  leopnmid  32490  csmdsymi  32686  chirredlem4  32745  sumdmdlem  32770  iundisjf  32934  iundisjfi  33141  nn0difffzod  33149  hashxpe  33152  xrpxdivcld  33254  gsumfs2d  33381  fldgensdrg  33635  lsmsnorb  33704  mxidlnzr  33750  zringfrac  33844  lactlmhm  34024  extdgval  34043  ccfldextdgrr  34062  ply1annprmidl  34097  pnfneige0  34341  rrhre  34411  esumcocn  34470  hasheuni  34475  sgon  34514  ddemeas  34626  dya2iocct  34670  dya2iocnrect  34671  eulerpartgbij  34762  eulerpartlemgs2  34770  coinflippv  34874  signstfvneq0  34959  hgt750lemb  35043  bnj1136  35385  bnj1175  35392  bnj1408  35424  fissorduni  35480  fnrelpredd  35482  dfscott3  35512  fineqvnttrclselem1  35534  fineqvnttrclse  35537  unir1regs  35548  axpowg2  35560  axpowg3  35561  onvf1od  35591  vonf1wev  35592  vonf1owevOLD  35594  pthhashvtx  35620  spthcycl  35621  upgracycumgr  35645  umgracycusgr  35646  cvmsdisj  35762  mrsubvrs  36014  mppspstlem  36063  problem4  36160  climuzcnv  36163  currybi  36180  dfon2lem7  36279  imageval  36420  filnetlem2  36890  lukshef-ax2  36926  arg-ax  36927  weiunpo  36976  axtco  36982  dfttc4lem2  37040  regsfromunir1  37051  bj-andnotim  37181  bj-modalbe  37313  bj-hbs1  37447  bj-hbsb2av  37449  bj-2uplex  37658  bj-axseprep  37711  mptsnunlem  37984  onsucuni3  38013  finixpnum  38256  fin2solem  38257  matunitlindflem2  38268  poimirlem6  38277  poimirlem7  38278  poimirlem8  38279  poimirlem18  38289  poimirlem21  38292  poimirlem22  38293  poimirlem32  38303  mblfinlem3  38310  itg2addnclem2  38323  itg2addnc  38325  heiborlem3  38464  ismndo2  38525  rngomndo  38586  isfld2  38656  isfldidl  38719  dmncan2  38728  oprabbi  38810  opabbi  38814  ac6s3f  38820  relcnveq3  38976  elrelscnveq3  39276  lsat0cv  39807  djavalN  41909  djhval  42172  dochkr1  42252  dochkr1OLDN  42253  hdmap1fval  42570  lcmineqlem13  42808  fiabv  43304  mhpind  43326  pellexlem5  43560  rmyabs  43685  jm2.24  43690  islssfgi  43799  pwslnm  43821  omlimcl2  43969  onexoegt  43971  rp-oelim2  44035  oeord2lim  44036  oeord2i  44037  ensucne0OLD  44256  iscard5  44262  clrellem  44348  frege114d  44484  frege55lem1a  44592  frege70  44659  gneispace  44860  ismnushort  45011  3impexpbicom  45189  ee3bir  45212  vk15.4j  45237  onfrALTlem2  45255  ax6e2nd  45267  dfvd1impr  45285  dfvd2impr  45313  e1bir  45339  e2bir  45342  e3bir  45447  suctrALT  45534  19.21a3con13vVD  45560  3impexpbicomVD  45565  tratrbVD  45569  ssralv2VD  45574  truniALTVD  45586  trintALTVD  45588  undif3VD  45590  csbingVD  45592  onfrALTlem3VD  45595  onfrALTlem2VD  45597  onfrALTVD  45599  csbsngVD  45601  csbxpgVD  45602  csbrngVD  45604  csbunigVD  45606  csbfv12gALTVD  45607  relopabVD  45609  ax6e2ndVD  45616  2uasbanhVD  45619  vk15.4jVD  45622  sspwimp  45626  sspwimpVD  45627  sspwimpcf  45628  sspwimpcfVD  45629  suctrALTcf  45630  suctrALTcfVD  45631  suctrALT3  45632  sspwimpALT  45633  unisnALT  45634  ax6e2ndALT  45638  isosctrlem1ALT  45642  iunconnlem2  45643  prclaxpr  45694  wfaxrep  45703  supminfxrrnmpt  46185  limsuppnflem  46424  limsupubuz  46427  cncfuni  46600  stoweidlem14  46728  stoweidlem35  46749  stoweidlem57  46771  stirlinglem7  46794  fourierdlem54  46874  etransclem32  46980  subsaliuncl  47072  meadjiunlem  47179  volmea  47188  caratheodory  47242  ovnsubaddlem2  47285  hoidmvlelem5  47313  hoiqssbllem2  47337  aibandbiaiaiffb  47632  funressnvmo  47782  dfdfat2  47865  afvres  47909  ndmaovass  47943  afv2res  47976  tz6.12-afv2  47977  el1fzopredsuc  48063  fundcmpsurinjimaid  48160  iccelpart  48182  lswn0  48193  ichnfimlem  48212  prprelb  48265  indprmfz  48382  evenprm2  48479  dfnbgr6  48622  dfsclnbgr6  48623  isgrtri  48708  grlimedgclnbgr  48760  idomcanr  49113  lincext1  49234  resinsnALT  49651  tposideq  49666  sepfsepc  49706  isclatd  49761  uprcl2  49967  functhincfun  50227  fullthinc  50228  setc2othin  50244  alsralrex  50590