Theorem biimpri 218

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 210. (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 214	. 2 ⊢ (𝜓 ↔ 𝜑)
3	2	biimpi 206	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  mpbir  221  sylibr  224  sylbir  225  sylbbr  226  sylbb1  227  sylbb2  228  syl5bir  233  syl6ibr  242  mtbi  311  dfbi  461  simplbi2  488  sylanbr  571  sylanblrc  578  sylan2br  582  pm2.54  841  orbi2i  898  pm2.31  908  pm2.85  918  pm3.11  977  pm3.2an3OLD  1425  syl3an1br  1512  syl3an2br  1513  syl3an3br  1514  had1  1690  nic-axALT  1747  speimfw  2045  sbbii  2056  ceqsexv2d  3395  eueq2  3532  ralun  3946  ssunieq  4608  ax6vsep  4919  opelxpi  5288  ordunidif  5916  unizlim  5987  dffo2  6260  dff1o2  6283  resdif  6298  f1o00  6312  fvimacnvALT  6479  fvcofneq  6510  exfo  6520  ressnop0  6563  fsnunfv  6597  2f1fvneq  6660  ovid  6924  ovidig  6925  dfwe2  7128  onminex  7154  nnsuc  7229  1stnpr  7319  2ndnpr  7320  f1stres  7339  f2ndres  7340  1st2val  7343  2nd2val  7344  frxp  7438  soxp  7441  tz7.49  7693  elixpsn  8101  domdifsn  8199  domunsncan  8216  fineqvlem  8330  unblem4  8371  ordiso2  8576  domwdom  8635  zfreg  8656  inf3lem3  8691  trcl  8768  unir1  8840  ssrankr1  8862  djuunxp  8947  pm54.43lem  9025  infxpenlem  9036  ween  9058  acni3  9070  kmlem1  9174  infdif  9233  ackbij1lem1  9244  fin23lem14  9357  fin23lem32  9368  isfin1-3  9410  axcc2lem  9460  axdc3lem2  9475  ac6c4  9505  zornn0g  9529  axdclem2  9544  rnct  9549  brdom3  9552  brdom5  9553  brdom4  9554  brdom6disj  9556  konigthlem  9592  pwcfsdom  9607  cfpwsdom  9608  alephom  9609  gruina  9842  grur1  9844  grothomex  9853  grothac  9854  nqpr  10038  axcnre  10187  axpre-sup  10192  ssxr  10309  le2tri3i  10369  muldivdir  10922  0nn0  11509  uzind4  11948  rpnnen1lem5  12021  rpnnen1lem5OLD  12027  elfz4  12542  eluzfz  12544  ssfzo12bi  12771  hashgt0elex  13391  hashxplem  13422  hashfun  13426  ishashinf  13449  ffz0iswrd  13528  wrdsymb1  13539  ccatfv0  13565  lswccats1fst  13620  ccatswrd  13665  repswfsts  13737  cshinj  13766  cshw1  13777  swrdco  13792  cotr2g  13925  xptrrel  13929  trclun  13963  resqrex  14199  pwm1geoser  14807  sumeven  15318  ndvdsadd  15342  gcdcllem1  15429  gcdcllem3  15431  lcmftp  15557  lcmfunsnlem2lem2  15560  lcmfunsnlem2  15561  lcmfun  15566  ncoprmgcdne1b  15571  coprmprod  15582  coprmproddvdslem  15583  divgcdcoprmex  15587  1idssfct  15600  prmodvdslcmf  15958  cshwrepswhash1  16016  xpsff1o  16436  initoeu2  16873  clatlem  17319  clatlubcl2  17321  clatglbcl2  17323  xpsmnd  17538  sgrp2rid2  17621  xpsgrp  17742  symgextf  18044  gsmsymgrfix  18055  gsmsymgreqlem2  18058  pmtr3ncom  18102  odlem1  18161  gexlem1  18201  dprdfeq0  18629  gsumdixp  18817  lspcl  19189  cply1mul  19879  psgndiflemB  20162  lindfind  20372  lindsind  20373  lindsind2  20375  lindff1  20376  f1linds  20381  gsumcom3fi  20423  mat1dimscm  20499  dmatmul  20521  mdetdiag  20623  mdetunilem7  20642  mdetunilem9  20644  madurid  20668  fvmptnn04if  20874  toprntopon  20950  tgcl  20994  elcls  21098  opnnei  21145  neiptopnei  21157  cnpnei  21289  cmpfii  21433  txcnp  21644  xpstps  21834  fbun  21864  isfild  21882  snfil  21888  filconn  21907  isufil2  21932  hauspwpwf1  22011  cnextcn  22091  ustfilxp  22236  ustuqtop4  22268  xpsxms  22559  xpsms  22560  rlmnvc  22727  nmoid  22766  xrsmopn  22835  xrhmeo  22965  cphsqrtcl  23203  iscmet3  23310  iundisj  23536  ioorinv  23564  plyexmo  24288  aalioulem3  24309  dvtaylp  24344  dvradcnv  24395  logtayllem  24626  logtayl  24627  logbid1  24727  logbchbase  24730  relogbcxpb  24746  logbmpt  24747  logbfval  24749  musum  25138  lgsmodeq  25288  lgsmulsqcoprm  25289  2lgs  25353  pntlem3  25519  nbupgrel  26464  nbusgrvtxm1  26504  nb3gr2nb  26509  cplgruvtxbOLD  26546  pthdivtx  26860  pthdlem2lem  26898  crctisclwlk  26925  wwlks  26963  wwlksonvtx  26985  wspthnonp  26993  wlkiswwlks2lem1  27003  wwlksnndef  27049  clwlkclwwlkf1lem3  27156  clwlkclwwlkf1  27160  clwwlknnn  27188  clwwlknfi  27201  clwwlkel  27202  clwwlkf1  27205  clwlksf1clwwlklemOLD  27249  clwwlknonwwlknonb  27281  umgr3v3e3cycl  27364  frgrncvvdeq  27491  sspval  27918  blo3i  27997  ajfval  28004  spanval  28532  cmcmlem  28790  leopnmid  29337  csmdsymi  29533  chirredlem4  29592  sumdmdlem  29617  difininv  29692  iundisjf  29740  padct  29837  iundisjfi  29895  fprodex01  29911  xrpxdivcld  29983  pnfneige0  30337  rrhre  30405  esumcocn  30482  hasheuni  30487  sgon  30527  sigapildsys  30565  ddemeas  30639  dya2iocct  30682  dya2iocnrect  30683  eulerpartgbij  30774  eulerpartlemgs2  30782  coinflippv  30885  hgt750lemb  31074  bnj1136  31403  bnj1175  31410  bnj1408  31442  cvmsdisj  31590  mrsubvrs  31757  mppspstlem  31806  problem4  31900  climuzcnv  31903  dford5  31946  dfon2lem7  32030  sltval2  32146  noxp1o  32153  conway  32247  scutbdaylt  32259  imageval  32374  filnetlem2  32711  df3nandALT1  32733  lukshef-ax2  32751  arg-ax  32752  bj-andnotim  32910  bj-modalbe  33015  bj-2uplex  33341  mptsnunlem  33522  onsucuni3  33552  finixpnum  33727  fin2solem  33728  matunitlindflem2  33739  poimirlem6  33748  poimirlem7  33749  poimirlem8  33750  poimirlem18  33760  poimirlem21  33763  poimirlem22  33764  poimirlem32  33774  mblfinlem3  33781  itg2addnclem2  33794  itg2addnc  33796  bddiblnc  33812  ftc1anclem6  33822  heiborlem3  33944  ismndo2  34005  rngomndo  34066  isfld2  34136  isfldidl  34199  dmncan2  34208  oprabbi  34302  opabbi  34306  ac6s3f  34311  relcnveq3  34435  elrelscnveq3  34583  lsat0cv  34842  pclfinclN  35758  docavalN  36933  djavalN  36945  dochval  37161  djhval  37208  dochexmidlem8  37277  dochkr1  37288  dochkr1OLDN  37289  hdmap1fval  37606  pellexlem5  37923  rmyabs  38051  jm2.24  38056  islssfgi  38168  pwslnm  38190  dgraaub  38244  clrellem  38455  frege114d  38576  frege55lem1a  38686  frege70  38753  gneispace  38958  3impexpbicom  39210  ee3bir  39234  vk15.4j  39259  onfrALTlem2  39286  ax6e2nd  39299  dfvd1impr  39317  dfvd2impr  39354  e1bir  39380  e2bir  39383  e3bir  39491  suctrALT  39583  19.21a3con13vVD  39609  3impexpbicomVD  39614  tratrbVD  39619  ssralv2VD  39624  truniALTVD  39636  trintALTVD  39638  undif3VD  39640  onfrALTlem3VD  39645  onfrALTlem2VD  39647  onfrALTVD  39649  relopabVD  39659  ax6e2ndVD  39666  2uasbanhVD  39669  vk15.4jVD  39672  sspwimp  39676  sspwimpVD  39677  sspwimpcf  39678  sspwimpcfVD  39679  suctrALTcf  39680  suctrALTcfVD  39681  suctrALT3  39682  sspwimpALT  39683  unisnALT  39684  ax6e2ndALT  39688  isosctrlem1ALT  39692  iunconnlem2  39693  supminfxrrnmpt  40217  limsuppnflem  40460  limsupubuz  40463  cncfuni  40617  iblcncfioo  40711  stoweidlem14  40748  stoweidlem17  40751  stoweidlem35  40769  stoweidlem57  40791  stirlinglem7  40814  stirlinglem10  40817  fourierdlem54  40894  fourierdlem62  40902  fourierdlem63  40903  fourierdlem65  40905  fourierdlem73  40913  fourierdlem80  40920  fourierdlem82  40922  fourierdlem101  40941  etransclem32  41000  ioorrnopnxr  41044  subsaliuncl  41093  meadjiunlem  41199  ismeannd  41201  voliunsge0lem  41206  volmea  41208  caratheodory  41262  ovnsubaddlem2  41305  hoidmvlelem5  41333  hoiqssbllem2  41357  iinhoiicc  41408  aibandbiaiaiffb  41582  dfdfat2  41731  afvres  41772  tz6.12-afv  41773  ndmaovass  41806  el1fzopredsuc  41863  fzoopth  41865  iccpartiltu  41886  iccelpart  41897  lswn0  41908  ccatpfx  41937  evenprm2  42151  lincext1  42771