Theorem biimpri 228

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  mpbir  231  sylibr  234  sylbir  235  sylbbr  236  sylbb1  237  sylbb2  238  biimtrrid  243  imbitrrdi  252  mtbi  322  sylnib  328  simplbi2  500  sylanbr  582  sylan2br  595  pm2.54  852  orbi2i  912  pm2.31  922  pm2.85  932  pm3.11  994  syl3an1br  1408  syl3an2br  1409  syl3an3br  1410  had1  1603  nic-axALT  1674  speimfw  1963  sbbii  2077  hbsbwOLD  2173  mobii  2541  mo4  2559  r19.30  3096  ceqsexv2dOLD  3489  eueq2  3670  ralun  4149  ssunieq  4893  ax6vsep  5242  opelxpi  5656  ordunidif  6357  unizlim  6431  dffo2  6740  dff1o2  6769  resdif  6785  f1o00  6799  fvimacnvALT  6991  fvcofneq  7027  exfo  7039  ressnop0  7087  fsnunfv  7123  2f1fvneq  7197  ovid  7490  ovidig  7491  dfwe2  7710  dford5  7720  onminex  7738  nnsuc  7817  1stnpr  7928  2ndnpr  7929  f1stres  7948  f2ndres  7949  1st2val  7952  2nd2val  7953  frxp  8059  soxp  8062  frxp2  8077  fprlem1  8233  tz7.49  8367  elixpsn  8864  domdifsn  8977  domunsncan  8994  unfi  9085  cnvfi  9090  fineqvlem  9155  unblem4  9184  ordiso2  9407  zfreg  9488  elirrv  9489  inf3lem3  9526  trcl  9624  unir1  9709  ssrankr1  9731  djuunxp  9817  pm54.43lem  9896  infxpenlem  9907  ween  9929  acni3  9941  kmlem1  10045  infdif  10102  ackbij1lem1  10113  fin23lem32  10238  isfin1-3  10280  axdc3lem2  10345  ac6c4  10375  zornn0g  10399  axdclem2  10414  rnct  10419  brdom3  10422  brdom5  10423  brdom4  10424  brdom6disj  10426  konigthlem  10462  pwcfsdom  10477  cfpwsdom  10478  alephom  10479  gruina  10712  grur1  10714  grothomex  10723  grothac  10724  nqpr  10908  axcnre  11058  axpre-sup  11063  ssxr  11185  le2tri3i  11246  muldivdir  11817  0nn0  12399  uzind4  12807  rpnnen1lem5  12882  elfz4  13420  eluzfz  13422  ssfzo12bi  13664  fzoopth  13665  hashgt0elex  14308  hashgt23el  14331  hashxplem  14340  hashfun  14344  ishashinf  14370  wrdsymb1  14460  ccatfv0  14490  lswccats1fst  14542  ccatswrd  14575  ccatpfx  14607  splfv1  14661  repswfsts  14687  cshinj  14717  swrdco  14744  cotr2g  14883  trclun  14921  resqrex  15157  sumeven  16298  ndvdsadd  16321  gcdcllem1  16410  gcdcllem3  16412  lcmftp  16547  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  divgcdcoprmex  16577  1idssfct  16591  prmodvdslcmf  16959  cshwrepswhash1  17014  xpsfrnel2  17468  xpsff1o  17471  catcone0  17593  initoeu2  17923  clatlem  18408  clatlubcl2  18410  clatglbcl2  18412  xpsmnd  18651  xpsgrp  18938  mulgfval  18948  gsmsymgrfix  19307  pmtr3ncom  19354  gsumcom3fi  19858  dprdfeq0  19903  gsumdixp  20204  lspcl  20879  lindfind  21723  lindsind  21724  lindsind2  21726  lindff1  21727  f1linds  21732  evls1maplmhm  22262  mat1dimscm  22360  mdetunilem7  22503  fvmptnn04if  22734  tgcl  22854  elcls  22958  opnnei  23005  neiptopnei  23017  cnpnei  23149  cmpfii  23294  txcnp  23505  xpstps  23695  fbun  23725  isfild  23743  snfil  23749  filconn  23768  isufil2  23793  hauspwpwf1  23872  cnextcn  23952  ustfilxp  24098  ustuqtop4  24130  xpsxms  24420  xpsms  24421  rlmnvc  24589  nmoid  24628  xrsmopn  24699  xrhmeo  24842  cphsqrtcl  25082  iscmet3  25191  iundisj  25447  ioorinv  25475  bddiblnc  25741  dvtaylp  26276  logbid1  26676  logbchbase  26679  relogbcxpb  26695  logbmpt  26696  logbfval  26698  musum  27099  lgsmodeq  27251  lgsmulsqcoprm  27252  2lgs  27316  2sqnn0  27347  pntlem3  27518  sltval2  27566  noxp1o  27573  conway  27710  scutbdaylt  27729  zsoring  28301  nbupgrel  29290  nbusgrvtxm1  29324  nb3gr2nb  29329  pthdivtx  29672  pthdlem2lem  29712  crctisclwlk  29739  wwlks  29780  wwlksonvtx  29800  wspthnonp  29804  wlkiswwlks2lem1  29814  wwlksnndef  29850  wwlksnfi  29851  clwlkclwwlkf1lem3  29950  clwlkclwwlkf1  29954  clwwlknnn  29977  clwwlkel  29990  clwwlkf1  29993  wwlksext2clwwlk  30001  clwwlknonwwlknonb  30050  umgr3v3e3cycl  30128  frgrncvvdeq  30253  sspval  30667  blo3i  30746  ajfval  30753  spanval  31277  cmcmlem  31535  leopnmid  32082  csmdsymi  32278  chirredlem4  32337  sumdmdlem  32362  iundisjf  32533  padct  32662  iundisjfi  32739  nn0difffzod  32749  hashxpe  32752  fprodex01  32770  xrpxdivcld  32875  gsumfs2d  33008  fldgensdrg  33253  lsmsnorb  33328  mxidlnzr  33404  zringfrac  33491  lactlmhm  33601  extdgval  33620  ccfldextdgrr  33639  ply1annprmidl  33674  pnfneige0  33918  rrhre  33988  esumcocn  34047  hasheuni  34052  sgon  34091  sigapildsys  34129  ddemeas  34203  dya2iocct  34248  dya2iocnrect  34249  eulerpartgbij  34340  eulerpartlemgs2  34348  coinflippv  34452  signstfvneq0  34540  hgt750lemb  34624  bnj1136  34964  bnj1175  34971  bnj1408  35003  fnrelpredd  35056  unir1regs  35068  onvf1od  35080  vonf1owev  35081  pthhashvtx  35101  spthcycl  35102  upgracycumgr  35126  umgracycusgr  35127  cvmsdisj  35243  mrsubvrs  35495  mppspstlem  35544  problem4  35641  climuzcnv  35644  currybi  35661  dfon2lem7  35763  imageval  35904  filnetlem2  36353  df3nandALT1  36373  lukshef-ax2  36389  arg-ax  36390  weiunpo  36439  bj-andnotim  36562  bj-modalbe  36662  bj-hbs1  36786  bj-hbsb2av  36788  bj-2uplex  36996  mptsnunlem  37312  onsucuni3  37341  fvineqsneq  37386  finixpnum  37585  fin2solem  37586  matunitlindflem2  37597  poimirlem6  37606  poimirlem7  37607  poimirlem8  37608  poimirlem18  37618  poimirlem21  37621  poimirlem22  37622  poimirlem32  37632  mblfinlem3  37639  itg2addnclem2  37652  itg2addnc  37654  ftc1anclem6  37678  heiborlem3  37793  ismndo2  37854  rngomndo  37915  isfld2  37985  isfldidl  38048  dmncan2  38057  oprabbi  38141  opabbi  38145  ac6s3f  38151  relcnveq3  38295  elrelscnveq3  38468  lsat0cv  39012  pclfinclN  39929  docavalN  41102  djavalN  41114  dochval  41330  djhval  41377  dochexmidlem8  41446  dochkr1  41457  dochkr1OLDN  41458  hdmap1fval  41775  lcmineqlem13  42014  unitscyglem4  42171  fiabv  42509  selvcllem5  42555  mhpind  42567  pellexlem5  42806  rmyabs  42931  jm2.24  42936  islssfgi  43045  pwslnm  43067  dgraaub  43121  omlimcl2  43215  onexoegt  43217  rp-oelim2  43281  oeord2lim  43282  oeord2i  43283  ensucne0OLD  43503  iscard5  43509  clrellem  43595  frege114d  43731  frege55lem1a  43839  frege70  43906  gneispace  44107  ismnushort  44274  3impexpbicom  44454  ee3bir  44477  vk15.4j  44502  onfrALTlem2  44520  ax6e2nd  44532  dfvd1impr  44550  dfvd2impr  44578  e1bir  44604  e2bir  44607  e3bir  44712  suctrALT  44799  19.21a3con13vVD  44825  3impexpbicomVD  44830  tratrbVD  44834  ssralv2VD  44839  truniALTVD  44851  trintALTVD  44853  undif3VD  44855  csbingVD  44857  onfrALTlem3VD  44860  onfrALTlem2VD  44862  onfrALTVD  44864  csbsngVD  44866  csbxpgVD  44867  csbrngVD  44869  csbunigVD  44871  csbfv12gALTVD  44872  relopabVD  44874  ax6e2ndVD  44881  2uasbanhVD  44884  vk15.4jVD  44887  sspwimp  44891  sspwimpVD  44892  sspwimpcf  44893  sspwimpcfVD  44894  suctrALTcf  44895  suctrALTcfVD  44896  suctrALT3  44897  sspwimpALT  44898  unisnALT  44899  ax6e2ndALT  44903  isosctrlem1ALT  44907  iunconnlem2  44908  prclaxpr  44959  wfaxrep  44968  supminfxrrnmpt  45450  limsuppnflem  45691  limsupubuz  45694  cncfuni  45867  iblcncfioo  45959  stoweidlem14  45995  stoweidlem17  45998  stoweidlem35  46016  stoweidlem57  46038  stirlinglem7  46061  stirlinglem10  46064  fourierdlem54  46141  fourierdlem62  46149  fourierdlem63  46150  fourierdlem65  46152  fourierdlem73  46160  fourierdlem80  46167  fourierdlem82  46169  fourierdlem101  46188  etransclem32  46247  ioorrnopnxr  46288  subsaliuncl  46339  meadjiunlem  46446  ismeannd  46448  voliunsge0lem  46453  volmea  46455  caratheodory  46509  ovnsubaddlem2  46552  hoidmvlelem5  46580  hoiqssbllem2  46604  iinhoiicc  46655  aibandbiaiaiffb  46879  funressnvmo  47029  dfdfat2  47112  afvres  47156  tz6.12-afv  47157  ndmaovass  47190  afv2res  47223  tz6.12-afv2  47224  el1fzopredsuc  47309  zp1modne  47330  fundcmpsurinjimaid  47395  iccpartiltu  47406  iccelpart  47417  lswn0  47428  ichnfimlem  47447  prprelb  47500  evenprm2  47698  dfnbgr6  47841  dfsclnbgr6  47842  isgrtri  47927  grlimedgclnbgr  47979  lincext1  48439  resinsnALT  48857  tposideq  48872  sepfsepc  48912  isclatd  48967  intubeu  48968  unilbeu  48969  uprcl2  49174  functhincfun  49434  fullthinc  49435  setc2othin  49451