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  2596  r19.30  3134  eueq2  3675  ralun  4151  ssunieq  4911  replem  5251  ax6vsep  5268  opelxpi  5700  ordunidif  6415  unizlim  6489  dffo2  6800  dff1o2  6830  resdif  6846  fvimacnvALT  7056  fvcofneq  7092  exfo  7104  ressnop0  7156  fsnunfv  7191  2f1fvneq  7263  ovid  7560  ovidig  7561  uniex2  7745  dfwe2  7779  dford5  7789  onminex  7807  nnsuc  7886  1stnpr  7996  2ndnpr  7997  1st2val  8020  2nd2val  8021  frxp  8128  soxp  8131  fprlem1  8303  tz7.49  8438  domdifsn  9055  domunsncan  9072  unfi  9162  cnvfi  9167  fineqvlem  9233  unblem4  9262  zfreg  9565  elirrvOLD  9567  inf3lem3  9606  unir1  9792  ssrankr1  9814  djuunxp  9923  pm54.43lem  10002  infxpenlem  10013  ween  10035  acni3  10047  kmlem1  10150  infdif  10207  ackbij1lem1  10218  fin23lem32  10343  isfin1-3  10385  axdc3lem2  10450  ac6c4  10480  zornn0g  10504  axdclem2  10519  rnct  10524  brdom3  10527  brdom5  10528  brdom4  10529  brdom6disj  10531  konigthlem  10568  pwcfsdom  10583  cfpwsdom  10584  alephom  10585  gruina  10818  grur1  10820  grothac  10830  nqpr  11014  axcnre  11164  ssxr  11294  le2tri3i  11355  muldivdir  11922  0nn0  12534  uzind4  12946  rpnnen1lem5  13021  elfz4  13561  eluzfz  13563  ssfzo12bi  13807  fzoopth  13808  hashgt0elex  14455  hashgt23el  14479  hashxplem  14488  hashfun  14492  ishashinf  14518  wrdsymb1  14608  ccatfv0  14639  lswccats1fst  14693  ccatswrd  14728  ccatpfx  14760  splfv1  14814  cshinj  14872  swrdco  14898  cotr2g  15037  trclun  15075  resqrex  15325  sumeven  16467  ndvdsadd  16490  gcdcllem1  16579  gcdcllem3  16581  lcmftp  16716  lcmfunsnlem2lem2  16719  lcmfunsnlem2  16720  divgcdcoprmex  16746  1idssfct  16760  prmodvdslcmf  17129  cshwrepswhash1  17184  xpsfrnel2  17640  xpsff1o  17643  catcone0  17765  initoeu2  18095  chnccat  18704  xpsmnd  18872  xpsgrp  19169  mulgfval  19179  gsmsymgrfix  19542  pmtr3ncom  19589  dprdfeq0  20138  gsumdixp  20446  lspcl  21147  lindsind2  22019  lindff1  22020  f1linds  22025  selvcllem5  22340  evls1maplmhm  22587  mat1dimscm  22682  tgcl  23176  elcls  23280  neiptopnei  23339  cmpfii  23616  txcnp  23828  xpstps  24018  fbun  24048  snfil  24072  filconn  24091  isufil2  24116  hauspwpwf1  24195  cnextcn  24275  ustfilxp  24421  ustuqtop4  24452  xpsxms  24742  xpsms  24743  rlmnvc  24911  nmoid  24950  xrsmopn  25021  xrhmeo  25156  cphsqrtcl  25394  iscmet3  25503  iundisj  25758  ioorinv  25786  bddiblnc  26052  dvtaylp  26584  logbid1  26984  logbchbase  26987  relogbcxpb  27003  logbmpt  27004  musum  27406  lgsmodeq  27557  lgsmulsqcoprm  27558  2lgs  27622  2sqnn0  27653  pntlem3  27824  ltsval2  27871  noxp1o  27878  cutbdaylt  28042  zsoring  28653  nb3gr2nb  29792  pthdivtx  30139  pthhashvtx  30142  pthdlem2lem  30180  crctisclwlk  30208  spthcycl  30219  wwlks  30251  wwlksonvtx  30271  wlkiswwlks2lem1  30285  wwlksnndef  30321  wwlksnfi  30322  clwlkclwwlkf1lem3  30424  clwlkclwwlkf1  30428  clwwlknnn  30451  clwwlkel  30464  wwlksext2clwwlk  30475  clwwlknonwwlknonb  30524  umgr3v3e3cycl  30606  frgrncvvdeq  30731  sspval  31146  blo3i  31225  ajfval  31232  spanval  31756  cmcmlem  32014  leopnmid  32561  csmdsymi  32757  chirredlem4  32816  sumdmdlem  32841  iundisjf  33005  iundisjfi  33211  nn0difffzod  33219  hashxpe  33222  xrpxdivcld  33324  gsumfs2d  33445  fldgensdrg  33699  lsmsnorb  33768  mxidlnzr  33814  zringfrac  33908  lactlmhm  34088  extdgval  34107  ccfldextdgrr  34126  ply1annprmidl  34161  pnfneige0  34405  rrhre  34475  esumcocn  34534  hasheuni  34539  sgon  34578  ddemeas  34691  dya2iocct  34735  dya2iocnrect  34736  eulerpartgbij  34827  eulerpartlemgs2  34835  coinflippv  34939  signstfvneq0  35024  hgt750lemb  35108  bnj1136  35450  bnj1175  35457  bnj1408  35489  fissorduni  35538  fnrelpredd  35540  dfscott3  35570  fineqvnttrclselem1  35591  fineqvnttrclse  35594  unir1regs  35605  axpowg2  35617  axpowg3  35618  onvf1od  35648  vonf1wev  35649  vonf1owevOLD  35651  upgracycumgr  35682  umgracycusgr  35683  cvmsdisj  35799  mrsubvrs  36051  mppspstlem  36100  problem4  36197  climuzcnv  36200  currybi  36217  dfon2lem7  36316  imageval  36457  filnetlem2  36947  lukshef-ax2  36983  arg-ax  36984  weiunpo  37033  axtco  37039  dfttc4lem2  37097  regsfromunir1  37108  bj-andnotim  37238  bj-modalbe  37370  bj-hbs1  37504  bj-hbsb2av  37506  bj-2uplex  37715  bj-axseprep  37768  mptsnunlem  38041  onsucuni3  38070  finixpnum  38313  fin2solem  38314  matunitlindflem2  38325  poimirlem6  38334  poimirlem7  38335  poimirlem8  38336  poimirlem18  38346  poimirlem21  38349  poimirlem22  38350  poimirlem32  38360  mblfinlem3  38367  itg2addnclem2  38380  itg2addnc  38382  heiborlem3  38522  ismndo2  38583  rngomndo  38644  isfld2  38714  isfldidl  38777  dmncan2  38786  oprabbi  38868  opabbi  38872  ac6s3f  38878  relcnveq3  39034  elrelscnveq3  39334  lsat0cv  39865  djavalN  41967  djhval  42230  dochkr1  42310  dochkr1OLDN  42311  hdmap1fval  42628  lcmineqlem13  42866  fiabv  43362  mhpind  43384  pellexlem5  43618  rmyabs  43743  jm2.24  43748  islssfgi  43857  pwslnm  43879  omlimcl2  44027  onexoegt  44029  rp-oelim2  44093  oeord2lim  44094  oeord2i  44095  ensucne0OLD  44314  iscard5  44320  clrellem  44406  frege114d  44542  frege55lem1a  44650  frege70  44717  gneispace  44918  ismnushort  45069  3impexpbicom  45247  ee3bir  45270  vk15.4j  45295  onfrALTlem2  45313  ax6e2nd  45325  dfvd1impr  45343  dfvd2impr  45371  e1bir  45397  e2bir  45400  e3bir  45505  suctrALT  45592  19.21a3con13vVD  45618  3impexpbicomVD  45623  tratrbVD  45627  ssralv2VD  45632  truniALTVD  45644  trintALTVD  45646  undif3VD  45648  csbingVD  45650  onfrALTlem3VD  45653  onfrALTlem2VD  45655  onfrALTVD  45657  csbsngVD  45659  csbxpgVD  45660  csbrngVD  45662  csbunigVD  45664  csbfv12gALTVD  45665  relopabVD  45667  ax6e2ndVD  45674  2uasbanhVD  45677  vk15.4jVD  45680  sspwimp  45684  sspwimpVD  45685  sspwimpcf  45686  sspwimpcfVD  45687  suctrALTcf  45688  suctrALTcfVD  45689  suctrALT3  45690  sspwimpALT  45691  unisnALT  45692  ax6e2ndALT  45696  isosctrlem1ALT  45700  iunconnlem2  45701  prclaxpr  45752  wfaxrep  45761  supminfxrrnmpt  46243  limsuppnflem  46482  limsupubuz  46485  cncfuni  46658  stoweidlem14  46786  stoweidlem35  46807  stoweidlem57  46829  stirlinglem7  46852  fourierdlem54  46932  etransclem32  47038  subsaliuncl  47130  meadjiunlem  47237  volmea  47246  caratheodory  47300  ovnsubaddlem2  47343  hoidmvlelem5  47371  hoiqssbllem2  47395  aibandbiaiaiffb  47690  funressnvmo  47840  dfdfat2  47923  afvres  47967  ndmaovass  48001  afv2res  48034  tz6.12-afv2  48035  el1fzopredsuc  48121  fundcmpsurinjimaid  48218  iccelpart  48240  lswn0  48251  ichnfimlem  48270  prprelb  48323  indprmfz  48440  evenprm2  48537  dfnbgr6  48680  dfsclnbgr6  48681  isgrtri  48766  grlimedgclnbgr  48818  idomcanr  49170  lincext1  49291  resinsnALT  49708  tposideq  49723  sepfsepc  49763  isclatd  49818  uprcl2  50024  functhincfun  50284  fullthinc  50285  setc2othin  50301  alsralrex  50647