Theorem biimpri 220

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  mpbir  223  sylibr  226  sylbir  227  sylbbr  228  sylbb1  229  sylbb2  230  syl5bir  235  syl6ibr  244  mtbi  314  dfbi  469  simplbi2  496  sylanbr  577  sylanblrc  584  sylan2br  588  pm2.54  841  orbi2i  899  pm2.31  909  pm2.85  919  pm3.11  978  pm3.2an3OLD  1397  syl3an1br  1474  syl3an2br  1475  syl3an3br  1476  had1  1661  nic-axALT  1718  speimfw  2007  sbbii  2019  ceqsexv2d  3445  eueq2  3592  ralun  4018  ssunieq  4709  ax6vsep  5023  opelxpi  5394  ordunidif  6026  unizlim  6094  dffo2  6372  dff1o2  6398  resdif  6413  f1o00  6427  fvimacnvALT  6601  fvcofneq  6633  exfo  6643  ressnop0  6688  fsnunfv  6726  ovid  7056  ovidig  7057  dfwe2  7261  onminex  7287  nnsuc  7362  1stnpr  7451  2ndnpr  7452  f1stres  7471  f2ndres  7472  1st2val  7475  2nd2val  7476  frxp  7570  soxp  7573  tz7.49  7825  elixpsn  8235  domdifsn  8333  domunsncan  8350  fineqvlem  8464  unblem4  8505  ordiso2  8711  zfreg  8791  inf3lem3  8826  trcl  8903  unir1  8975  ssrankr1  8997  djuunxp  9082  pm54.43lem  9160  infxpenlem  9171  ween  9193  acni3  9205  kmlem1  9309  infdif  9368  ackbij1lem1  9379  fin23lem32  9503  isfin1-3  9545  axdc3lem2  9610  ac6c4  9640  zornn0g  9664  axdclem2  9679  rnct  9684  brdom3  9687  brdom5  9688  brdom4  9689  brdom6disj  9691  konigthlem  9727  pwcfsdom  9742  cfpwsdom  9743  alephom  9744  gruina  9977  grur1  9979  grothomex  9988  grothac  9989  nqpr  10173  axcnre  10323  axpre-sup  10328  ssxr  10448  le2tri3i  10508  muldivdir  11070  0nn0  11663  uzind4  12056  rpnnen1lem5  12132  elfz4  12656  eluzfz  12658  ssfzo12bi  12886  hashgt0elex  13507  hashxplem  13538  hashfun  13542  ishashinf  13565  ffz0iswrdOLD  13634  wrdsymb1  13647  ccatfv0  13677  lswccats1fst  13729  ccatswrd  13780  ccatpfx  13814  repswfsts  13931  cshinj  13966  swrdco  13992  cotr2g  14128  trclun  14166  resqrex  14402  pwm1geoser  15008  sumeven  15521  ndvdsadd  15544  gcdcllem1  15631  gcdcllem3  15633  lcmftp  15759  lcmfunsnlem2lem2  15762  lcmfunsnlem2  15763  lcmfun  15768  coprmprod  15784  coprmproddvdslem  15785  divgcdcoprmex  15789  1idssfct  15802  prmodvdslcmf  16159  cshwrepswhash1  16212  xpsff1o  16618  initoeu2  17055  clatlem  17501  clatlubcl2  17503  clatglbcl2  17505  xpsmnd  17720  xpsgrp  17925  gsmsymgrfix  18235  gsmsymgreqlem2  18238  pmtr3ncom  18282  dprdfeq0  18812  gsumdixp  19000  lspcl  19375  psgndiflemB  20346  lindfind  20563  lindsind  20564  lindsind2  20566  lindff1  20567  f1linds  20572  gsumcom3fi  20614  mat1dimscm  20690  dmatmul  20712  mdetdiag  20814  mdetunilem7  20833  mdetunilem9  20835  madurid  20859  fvmptnn04if  21065  toprntopon  21141  tgcl  21185  elcls  21289  opnnei  21336  neiptopnei  21348  cnpnei  21480  cmpfii  21625  txcnp  21836  xpstps  22026  fbun  22056  isfild  22074  snfil  22080  filconn  22099  isufil2  22124  hauspwpwf1  22203  cnextcn  22283  ustfilxp  22428  ustuqtop4  22460  xpsxms  22751  xpsms  22752  rlmnvc  22919  nmoid  22958  xrsmopn  23027  xrhmeo  23157  cphsqrtcl  23395  iscmet3  23503  iundisj  23756  ioorinv  23784  plyexmo  24509  aalioulem3  24530  dvtaylp  24565  dvradcnv  24616  logtayllem  24846  logtayl  24847  logbid1  24950  logbchbase  24953  relogbcxpb  24969  logbmpt  24970  logbfval  24972  musum  25373  lgsmodeq  25523  lgsmulsqcoprm  25524  2lgs  25588  pntlem3  25754  nbupgrel  26696  nbusgrvtxm1  26731  nb3gr2nb  26736  pthdivtx  27085  pthdlem2lem  27123  crctisclwlk  27150  wwlks  27188  wwlksonvtx  27208  wspthnonp  27212  wlkiswwlks2lem1  27222  wwlksnndef  27281  wwlksnfi  27282  clwlkclwwlkf1lem3  27393  clwlkclwwlkf1lem3OLD  27394  clwlkclwwlkf1OLD  27398  clwlkclwwlkf1  27402  clwwlknnn  27426  clwwlknfiOLD  27440  clwwlkel  27441  clwwlkf1OLD  27444  clwwlkf1  27449  clwwlknonwwlknonb  27512  umgr3v3e3cycl  27591  frgrncvvdeq  27721  sspval  28154  blo3i  28233  ajfval  28240  spanval  28768  cmcmlem  29026  leopnmid  29573  csmdsymi  29769  chirredlem4  29828  sumdmdlem  29853  difininv  29920  iundisjf  29969  padct  30067  iundisjfi  30123  fprodex01  30139  xrpxdivcld  30209  pnfneige0  30599  rrhre  30667  esumcocn  30744  hasheuni  30749  sgon  30789  sigapildsys  30827  ddemeas  30901  dya2iocct  30944  dya2iocnrect  30945  eulerpartgbij  31036  eulerpartlemgs2  31044  coinflippv  31148  hgt750lemb  31340  bnj1136  31668  bnj1175  31675  bnj1408  31707  cvmsdisj  31855  mrsubvrs  32022  mppspstlem  32071  problem4  32163  climuzcnv  32166  dford5  32209  dfon2lem7  32286  sltval2  32402  noxp1o  32409  conway  32503  scutbdaylt  32515  imageval  32630  filnetlem2  32966  df3nandALT1  32986  lukshef-ax2  33001  arg-ax  33002  bj-andnotim  33156  bj-modalbe  33271  bj-2uplex  33586  mptsnunlem  33784  onsucuni3  33813  finixpnum  34024  fin2solem  34025  matunitlindflem2  34037  poimirlem6  34046  poimirlem7  34047  poimirlem8  34048  poimirlem18  34058  poimirlem21  34061  poimirlem22  34062  poimirlem32  34072  mblfinlem3  34079  itg2addnclem2  34092  itg2addnc  34094  bddiblnc  34110  ftc1anclem6  34120  heiborlem3  34241  ismndo2  34302  rngomndo  34363  isfld2  34433  isfldidl  34496  dmncan2  34505  oprabbi  34597  opabbi  34601  ac6s3f  34607  relcnveq3  34725  elrelscnveq3  34874  lsat0cv  35192  pclfinclN  36109  docavalN  37282  djavalN  37294  dochval  37510  djhval  37557  dochexmidlem8  37626  dochkr1  37637  dochkr1OLDN  37638  hdmap1fval  37955  pellexlem5  38367  rmyabs  38494  jm2.24  38499  islssfgi  38611  pwslnm  38633  dgraaub  38687  clrellem  38896  frege114d  39017  frege55lem1a  39126  frege70  39193  gneispace  39398  3impexpbicom  39649  ee3bir  39673  vk15.4j  39698  onfrALTlem2  39716  ax6e2nd  39728  dfvd1impr  39746  dfvd2impr  39783  e1bir  39809  e2bir  39812  e3bir  39918  suctrALT  40005  19.21a3con13vVD  40031  3impexpbicomVD  40036  tratrbVD  40040  ssralv2VD  40045  truniALTVD  40057  trintALTVD  40059  undif3VD  40061  onfrALTlem3VD  40066  onfrALTlem2VD  40068  onfrALTVD  40070  relopabVD  40080  ax6e2ndVD  40087  2uasbanhVD  40090  vk15.4jVD  40093  sspwimp  40097  sspwimpVD  40098  sspwimpcf  40099  sspwimpcfVD  40100  suctrALTcf  40101  suctrALTcfVD  40102  suctrALT3  40103  sspwimpALT  40104  unisnALT  40105  ax6e2ndALT  40109  isosctrlem1ALT  40113  iunconnlem2  40114  supminfxrrnmpt  40616  limsuppnflem  40860  limsupubuz  40863  cncfuni  41037  iblcncfioo  41131  stoweidlem14  41168  stoweidlem17  41171  stoweidlem35  41189  stoweidlem57  41211  stirlinglem7  41234  stirlinglem10  41237  fourierdlem54  41314  fourierdlem62  41322  fourierdlem63  41323  fourierdlem65  41325  fourierdlem73  41333  fourierdlem80  41340  fourierdlem82  41342  fourierdlem101  41361  etransclem32  41420  ioorrnopnxr  41461  subsaliuncl  41510  meadjiunlem  41616  ismeannd  41618  voliunsge0lem  41623  volmea  41625  caratheodory  41679  ovnsubaddlem2  41722  hoidmvlelem5  41750  hoiqssbllem2  41774  iinhoiicc  41825  aibandbiaiaiffb  41999  funressnvmo  42119  dfdfat2  42179  afvres  42223  tz6.12-afv  42224  ndmaovass  42257  afv2res  42290  tz6.12-afv2  42291  el1fzopredsuc  42377  fzoopth  42379  iccpartiltu  42400  iccelpart  42411  lswn0  42422  prprelb  42465  evenprm2  42658  lincext1  43268