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  312  pm2.54  389  sylanbr  490  sylan2br  493  pm3.11  520  orbi2i  541  pm2.31  547  simplbi2  655  dfbi  661  sylanblrc  697  pm2.85  898  pm3.2an3  1240  syl3an1br  1365  syl3an2br  1366  syl3an3br  1367  had1  1542  nic-axALT  1599  speimfw  1876  sbbii  1887  ceqsexv2d  3243  eueq2  3380  ralun  3795  ssunieq  4472  ax6vsep  4785  opelxpi  5148  elsnxpOLD  5678  ordunidif  5773  unizlim  5844  funtpgOLD  5943  dffo2  6119  dff1o2  6142  resdif  6157  f1o00  6171  fvimacnvALT  6336  fvcofneq  6367  exfo  6377  ressnop0  6420  fsnunfv  6453  2f1fvneq  6517  ovid  6777  ovidig  6778  dfwe2  6981  onminex  7007  nnsuc  7082  1stnpr  7172  2ndnpr  7173  f1stres  7190  f2ndres  7191  1st2val  7194  2nd2val  7195  frxp  7287  soxp  7290  tz7.49  7540  elixpsn  7947  domdifsn  8043  domunsncan  8060  fineqvlem  8174  unblem4  8215  ordiso2  8420  domwdom  8479  zfreg  8500  inf3lem3  8527  trcl  8604  unir1  8676  ssrankr1  8698  pm54.43lem  8825  infxpenlem  8836  ween  8858  acni3  8870  kmlem1  8972  infdif  9031  ackbij1lem1  9042  fin23lem14  9155  fin23lem32  9166  isfin1-3  9208  axcc2lem  9258  axdc3lem2  9273  ac6c4  9303  zornn0g  9327  axdclem2  9342  rnct  9347  brdom3  9350  brdom5  9351  brdom4  9352  brdom6disj  9354  konigthlem  9390  pwcfsdom  9405  cfpwsdom  9406  alephom  9407  gruina  9640  grur1  9642  grothomex  9651  grothac  9652  nqpr  9836  axcnre  9985  axpre-sup  9990  ssxr  10107  le2tri3i  10167  muldivdir  10720  0nn0  11307  uzind4  11746  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  elfz4  12335  eluzfz  12337  ssfzo12bi  12563  hashgt0elex  13189  hashxplem  13220  hashfun  13224  ishashinf  13247  ffz0iswrd  13332  wrdsymb1  13342  ccatfv0  13367  lswccats1fst  13412  ccatswrd  13456  repswfsts  13528  cshinj  13557  cshw1  13568  swrdco  13583  cotr2g  13715  xptrrel  13719  trclun  13755  resqrex  13991  pwm1geoser  14600  sumeven  15110  ndvdsadd  15134  gcdcllem1  15221  gcdcllem3  15223  lcmftp  15349  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  lcmfun  15358  ncoprmgcdne1b  15363  coprmprod  15375  coprmproddvdslem  15376  divgcdcoprmex  15380  1idssfct  15393  prmodvdslcmf  15751  cshwrepswhash1  15809  xpsff1o  16228  initoeu2  16666  clatlem  17111  clatlubcl2  17113  clatglbcl2  17115  xpsmnd  17330  sgrp2rid2  17413  xpsgrp  17534  symg2bas  17818  symgextf  17837  gsmsymgrfix  17848  gsmsymgreqlem2  17851  pmtr3ncom  17895  odlem1  17954  gexlem1  17994  dprdfeq0  18421  gsumdixp  18609  lspcl  18976  cply1mul  19664  psgndiflemB  19946  lindfind  20155  lindsind  20156  lindsind2  20158  lindff1  20159  f1linds  20164  gsumcom3fi  20206  mat1dimscm  20281  dmatmul  20303  mdetdiag  20405  mdetunilem7  20424  mdetunilem9  20426  madurid  20450  fvmptnn04if  20654  toprntopon  20729  tgcl  20773  elcls  20877  opnnei  20924  neiptopnei  20936  cnpnei  21068  cmpfii  21212  txcnp  21423  xpstps  21613  fbun  21644  isfild  21662  snfil  21668  filconn  21687  isufil2  21712  hauspwpwf1  21791  cnextcn  21871  ustfilxp  22016  ustuqtop4  22048  xpsxms  22339  xpsms  22340  rlmnvc  22507  nmoid  22546  xrsmopn  22615  xrhmeo  22745  cphsqrtcl  22984  iscmet3  23091  iundisj  23316  ioorinv  23344  plyexmo  24068  aalioulem3  24089  dvtaylp  24124  dvradcnv  24175  logtayllem  24405  logtayl  24406  logbid1  24506  logbchbase  24509  relogbcxpb  24525  logbmpt  24526  logbfval  24528  musum  24917  lgsmodeq  25067  lgsmulsqcoprm  25068  2lgs  25132  pntlem3  25298  nbupgrel  26241  nbusgrvtxm1  26281  nb3gr2nb  26286  cplgruvtxb  26311  pthdivtx  26625  pthdlem2lem  26663  crctisclwlk  26689  wwlks  26727  wspthnonp  26744  wlkiswwlks2lem1  26755  wwlksnndef  26800  clwwlksnfi  26913  clwwlksel  26914  clwwlksf1  26917  clwlksf1clwwlklem  26968  umgr3v3e3cycl  27044  frgrncvvdeq  27173  sspval  27578  blo3i  27657  ajfval  27664  spanval  28192  cmcmlem  28450  leopnmid  28997  csmdsymi  29193  chirredlem4  29252  sumdmdlem  29277  difininv  29354  iundisjf  29402  padct  29497  iundisjfi  29555  fprodex01  29571  xrpxdivcld  29643  pnfneige0  29997  rrhre  30065  esumcocn  30142  hasheuni  30147  sgon  30187  sigapildsys  30225  ddemeas  30299  dya2iocct  30342  dya2iocnrect  30343  eulerpartgbij  30434  eulerpartlemgs2  30442  coinflippv  30545  hgt750lemb  30734  bnj1136  31065  bnj1175  31072  bnj1408  31104  cvmsdisj  31252  mrsubvrs  31419  mppspstlem  31468  problem4  31562  climuzcnv  31565  dford5  31608  dfon2lem7  31694  sltval2  31809  noxp1o  31816  conway  31910  scutbdaylt  31922  imageval  32037  filnetlem2  32374  df3nandALT1  32396  lukshef-ax2  32414  arg-ax  32415  bj-andnotim  32573  bj-modalbe  32678  bj-2uplex  33010  mptsnunlem  33185  onsucuni3  33215  finixpnum  33394  fin2solem  33395  matunitlindflem2  33406  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem32  33441  mblfinlem3  33448  itg2addnclem2  33462  itg2addnc  33464  bddiblnc  33480  ftc1anclem6  33490  heiborlem3  33612  ismndo2  33673  rngomndo  33734  isfld2  33804  isfldidl  33867  dmncan2  33876  oprabbi  33970  opabbi  33974  ac6s3f  33979  relcnveq3  34092  lsat0cv  34320  pclfinclN  35236  docavalN  36412  djavalN  36424  dochval  36640  djhval  36687  dochexmidlem8  36756  dochkr1  36767  dochkr1OLDN  36768  hdmap1fval  37086  pellexlem5  37397  rmyabs  37525  jm2.24  37530  islssfgi  37642  pwslnm  37664  dgraaub  37718  clrellem  37929  frege114d  38050  frege55lem1a  38160  frege70  38227  gneispace  38432  3impexpbicom  38685  ee3bir  38709  vk15.4j  38734  onfrALTlem2  38761  ax6e2nd  38774  dfvd1impr  38792  dfvd2impr  38829  e1bir  38855  e2bir  38858  e3bir  38966  suctrALT  39061  19.21a3con13vVD  39087  3impexpbicomVD  39092  tratrbVD  39097  ssralv2VD  39102  truniALTVD  39114  trintALTVD  39116  undif3VD  39118  onfrALTlem3VD  39123  onfrALTlem2VD  39125  onfrALTVD  39127  relopabVD  39137  ax6e2ndVD  39144  2uasbanhVD  39147  vk15.4jVD  39150  sspwimp  39154  sspwimpVD  39155  sspwimpcf  39156  sspwimpcfVD  39157  suctrALTcf  39158  suctrALTcfVD  39159  suctrALT3  39160  sspwimpALT  39161  unisnALT  39162  ax6e2ndALT  39166  isosctrlem1ALT  39170  iunconnlem2  39171  supminfxrrnmpt  39701  limsuppnflem  39942  limsupubuz  39945  cncfuni  40099  iblcncfioo  40194  stoweidlem14  40231  stoweidlem17  40234  stoweidlem35  40252  stoweidlem57  40274  stirlinglem7  40297  stirlinglem10  40300  fourierdlem54  40377  fourierdlem62  40385  fourierdlem63  40386  fourierdlem65  40388  fourierdlem73  40396  fourierdlem80  40403  fourierdlem82  40405  fourierdlem101  40424  etransclem32  40483  ioorrnopnxr  40527  subsaliuncl  40576  meadjiunlem  40682  ismeannd  40684  voliunsge0lem  40689  volmea  40691  caratheodory  40742  ovnsubaddlem2  40785  hoidmvlelem5  40813  hoiqssbllem2  40837  iinhoiicc  40888  aibandbiaiaiffb  41062  dfdfat2  41211  afvres  41252  tz6.12-afv  41253  ndmaovass  41286  el1fzopredsuc  41335  fzoopth  41337  iccpartiltu  41358  iccelpart  41369  lswn0  41380  ccatpfx  41409  evenprm2  41623  lincext1  42243