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  1431  syl3an2br  1432  syl3an3br  1433  had1  1630  nic-axALT  1701  speimfw  1990  sbbii  2116  mo4  2600  r19.30  3138  eueq2  3682  ralun  4159  ssunieq  4913  replem  5253  ax6vsep  5268  opelxpi  5699  ordunidif  6412  unizlim  6486  dffo2  6797  dff1o2  6827  resdif  6843  fvimacnvALT  7053  fvcofneq  7089  exfo  7101  ressnop0  7151  fsnunfv  7186  2f1fvneq  7259  ovid  7552  ovidig  7553  dfwe2  7772  dford5  7782  onminex  7800  nnsuc  7879  1stnpr  7989  2ndnpr  7990  1st2val  8013  2nd2val  8014  frxp  8121  soxp  8124  fprlem1  8296  tz7.49  8431  domdifsn  9047  domunsncan  9064  unfi  9154  cnvfi  9159  fineqvlem  9225  unblem4  9254  zfreg  9557  elirrvOLD  9559  inf3lem3  9598  unir1  9784  ssrankr1  9806  djuunxp  9906  pm54.43lem  9985  infxpenlem  9996  ween  10018  acni3  10030  kmlem1  10133  infdif  10190  ackbij1lem1  10201  fin23lem32  10327  isfin1-3  10369  axdc3lem2  10434  ac6c4  10464  zornn0g  10488  axdclem2  10503  rnct  10508  brdom3  10511  brdom5  10512  brdom4  10513  brdom6disj  10515  konigthlem  10552  pwcfsdom  10567  cfpwsdom  10568  alephom  10569  gruina  10802  grur1  10804  grothac  10814  nqpr  10998  axcnre  11148  ssxr  11278  le2tri3i  11339  muldivdir  11906  0nn0  12518  uzind4  12929  rpnnen1lem5  13004  elfz4  13544  eluzfz  13546  ssfzo12bi  13789  fzoopth  13790  hashgt0elex  14436  hashgt23el  14460  hashxplem  14469  hashfun  14473  ishashinf  14499  wrdsymb1  14589  ccatfv0  14620  lswccats1fst  14672  ccatswrd  14705  ccatpfx  14737  splfv1  14791  cshinj  14847  swrdco  14873  cotr2g  15012  trclun  15050  resqrex  15300  sumeven  16444  ndvdsadd  16467  gcdcllem1  16556  gcdcllem3  16558  lcmftp  16693  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  divgcdcoprmex  16723  1idssfct  16737  prmodvdslcmf  17106  cshwrepswhash1  17161  xpsfrnel2  17617  xpsff1o  17620  catcone0  17742  initoeu2  18072  chnccat  18681  xpsmnd  18834  xpsgrp  19124  mulgfval  19134  gsmsymgrfix  19497  pmtr3ncom  19544  dprdfeq0  20093  gsumdixp  20399  lspcl  21074  lindsind2  21937  lindff1  21938  f1linds  21943  selvcllem5  22258  evls1maplmhm  22505  mat1dimscm  22600  tgcl  23094  elcls  23198  neiptopnei  23257  cmpfii  23534  txcnp  23745  xpstps  23935  fbun  23965  snfil  23989  filconn  24008  isufil2  24033  hauspwpwf1  24112  cnextcn  24192  ustfilxp  24338  ustuqtop4  24369  xpsxms  24659  xpsms  24660  rlmnvc  24828  nmoid  24867  xrsmopn  24938  xrhmeo  25073  cphsqrtcl  25311  iscmet3  25420  iundisj  25675  ioorinv  25703  bddiblnc  25969  dvtaylp  26498  logbid1  26898  logbchbase  26901  relogbcxpb  26917  logbmpt  26918  musum  27320  lgsmodeq  27471  lgsmulsqcoprm  27472  2lgs  27536  2sqnn0  27567  pntlem3  27738  ltsval2  27785  noxp1o  27792  cutbdaylt  27956  zsoring  28567  nb3gr2nb  29674  pthdivtx  30016  pthdlem2lem  30056  crctisclwlk  30083  wwlks  30124  wwlksonvtx  30144  wlkiswwlks2lem1  30158  wwlksnndef  30194  wwlksnfi  30195  clwlkclwwlkf1lem3  30297  clwlkclwwlkf1  30301  clwwlknnn  30324  clwwlkel  30337  wwlksext2clwwlk  30348  clwwlknonwwlknonb  30397  umgr3v3e3cycl  30475  frgrncvvdeq  30600  sspval  31015  blo3i  31094  ajfval  31101  spanval  31625  cmcmlem  31883  leopnmid  32430  csmdsymi  32626  chirredlem4  32685  sumdmdlem  32710  iundisjf  32874  iundisjfi  33081  nn0difffzod  33089  hashxpe  33092  xrpxdivcld  33194  gsumfs2d  33321  fldgensdrg  33577  lsmsnorb  33647  mxidlnzr  33694  zringfrac  33788  lactlmhm  33968  extdgval  33987  ccfldextdgrr  34006  ply1annprmidl  34041  pnfneige0  34285  rrhre  34355  esumcocn  34414  hasheuni  34419  sgon  34458  ddemeas  34570  dya2iocct  34614  dya2iocnrect  34615  eulerpartgbij  34706  eulerpartlemgs2  34714  coinflippv  34818  signstfvneq0  34903  hgt750lemb  34987  bnj1136  35329  bnj1175  35336  bnj1408  35368  fissorduni  35422  fnrelpredd  35424  fineqvnttrclselem1  35456  fineqvnttrclse  35459  unir1regs  35470  axpowg2  35482  axpowg3  35483  onvf1od  35489  vonf1wev  35490  vonf1owevOLD  35492  pthhashvtx  35518  spthcycl  35519  upgracycumgr  35543  umgracycusgr  35544  cvmsdisj  35660  mrsubvrs  35912  mppspstlem  35961  problem4  36058  climuzcnv  36061  currybi  36078  dfon2lem7  36177  imageval  36318  filnetlem2  36778  lukshef-ax2  36814  arg-ax  36815  weiunpo  36864  axtco  36870  dfttc4lem2  36928  regsfromunir1  36939  bj-andnotim  37069  bj-modalbe  37201  bj-hbs1  37335  bj-hbsb2av  37337  bj-2uplex  37545  bj-axseprep  37598  mptsnunlem  37871  onsucuni3  37900  finixpnum  38143  fin2solem  38144  matunitlindflem2  38155  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem18  38176  poimirlem21  38179  poimirlem22  38180  poimirlem32  38190  mblfinlem3  38197  itg2addnclem2  38210  itg2addnc  38212  heiborlem3  38351  ismndo2  38412  rngomndo  38473  isfld2  38543  isfldidl  38606  dmncan2  38615  oprabbi  38699  opabbi  38703  ac6s3f  38709  relcnveq3  38865  elrelscnveq3  39165  lsat0cv  39696  djavalN  41798  djhval  42061  dochkr1  42141  dochkr1OLDN  42142  hdmap1fval  42459  lcmineqlem13  42697  fiabv  43195  mhpind  43217  pellexlem5  43451  rmyabs  43576  jm2.24  43581  islssfgi  43690  pwslnm  43712  omlimcl2  43860  onexoegt  43862  rp-oelim2  43926  oeord2lim  43927  oeord2i  43928  ensucne0OLD  44147  iscard5  44153  clrellem  44239  frege114d  44375  frege55lem1a  44483  frege70  44550  gneispace  44751  ismnushort  44902  3impexpbicom  45080  ee3bir  45103  vk15.4j  45128  onfrALTlem2  45146  ax6e2nd  45158  dfvd1impr  45176  dfvd2impr  45204  e1bir  45230  e2bir  45233  e3bir  45338  suctrALT  45425  19.21a3con13vVD  45451  3impexpbicomVD  45456  tratrbVD  45460  ssralv2VD  45465  truniALTVD  45477  trintALTVD  45479  undif3VD  45481  csbingVD  45483  onfrALTlem3VD  45486  onfrALTlem2VD  45488  onfrALTVD  45490  csbsngVD  45492  csbxpgVD  45493  csbrngVD  45495  csbunigVD  45497  csbfv12gALTVD  45498  relopabVD  45500  ax6e2ndVD  45507  2uasbanhVD  45510  vk15.4jVD  45513  sspwimp  45517  sspwimpVD  45518  sspwimpcf  45519  sspwimpcfVD  45520  suctrALTcf  45521  suctrALTcfVD  45522  suctrALT3  45523  sspwimpALT  45524  unisnALT  45525  ax6e2ndALT  45529  isosctrlem1ALT  45533  iunconnlem2  45534  prclaxpr  45585  wfaxrep  45594  supminfxrrnmpt  46076  limsuppnflem  46315  limsupubuz  46318  cncfuni  46491  stoweidlem14  46619  stoweidlem35  46640  stoweidlem57  46662  stirlinglem7  46685  fourierdlem54  46765  etransclem32  46871  subsaliuncl  46963  meadjiunlem  47070  volmea  47079  caratheodory  47133  ovnsubaddlem2  47176  hoidmvlelem5  47204  hoiqssbllem2  47228  aibandbiaiaiffb  47520  funressnvmo  47670  dfdfat2  47753  afvres  47797  ndmaovass  47831  afv2res  47864  tz6.12-afv2  47865  el1fzopredsuc  47951  fundcmpsurinjimaid  48048  iccelpart  48070  lswn0  48081  ichnfimlem  48100  prprelb  48153  indprmfz  48270  evenprm2  48367  dfnbgr6  48510  dfsclnbgr6  48511  isgrtri  48596  grlimedgclnbgr  48648  lincext1  49118  resinsnALT  49535  tposideq  49550  sepfsepc  49590  isclatd  49645  uprcl2  49851  functhincfun  50111  fullthinc  50112  setc2othin  50128