Theorem biimpri 230

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  mpbir  233  sylibr  236  sylbir  237  sylbbr  238  sylbb1  239  sylbb2  240  biimtrrid  245  imbitrrdi  254  mtbi  324  sylnib  330  simplbi2  504  biranri  509  bilanri  510  sylanbr  591  sylan2br  604  pm2.54  863  orbi2i  923  pm2.31  933  pm2.85  943  pm3.11  1006  syl3an1br  1425  syl3an2br  1426  syl3an3br  1427  had1  1623  nic-axALT  1694  speimfw  1983  sbbii  2109  mo4  2593  r19.30  3129  eueq2  3673  ralun  4150  ssunieq  4902  replem  5238  ax6vsep  5253  opelxpi  5684  ordunidif  6396  unizlim  6470  dffo2  6782  dff1o2  6812  resdif  6828  fvimacnvALT  7038  fvcofneq  7074  exfo  7086  ressnop0  7136  fsnunfv  7171  2f1fvneq  7244  ovid  7537  ovidig  7538  dfwe2  7757  dford5  7767  onminex  7785  nnsuc  7864  1stnpr  7974  2ndnpr  7975  1st2val  7998  2nd2val  7999  frxp  8106  soxp  8109  fprlem1  8281  tz7.49  8416  domdifsn  9032  domunsncan  9049  unfi  9139  cnvfi  9144  fineqvlem  9210  unblem4  9239  zfreg  9544  elirrvOLD  9546  inf3lem3  9585  unir1  9771  ssrankr1  9793  djuunxp  9879  pm54.43lem  9958  infxpenlem  9969  ween  9991  acni3  10003  kmlem1  10107  infdif  10164  ackbij1lem1  10175  fin23lem32  10301  isfin1-3  10343  axdc3lem2  10408  ac6c4  10438  zornn0g  10462  axdclem2  10477  rnct  10482  brdom3  10485  brdom5  10486  brdom4  10487  brdom6disj  10489  konigthlem  10526  pwcfsdom  10541  cfpwsdom  10542  alephom  10543  gruina  10776  grur1  10778  grothac  10788  nqpr  10972  axcnre  11122  ssxr  11252  le2tri3i  11313  muldivdir  11883  0nn0  12496  uzind4  12907  rpnnen1lem5  12982  elfz4  13522  eluzfz  13524  ssfzo12bi  13767  fzoopth  13768  hashgt0elex  14414  hashgt23el  14437  hashxplem  14446  hashfun  14450  ishashinf  14476  wrdsymb1  14566  ccatfv0  14597  lswccats1fst  14649  ccatswrd  14682  ccatpfx  14714  splfv1  14768  cshinj  14824  swrdco  14850  cotr2g  14989  trclun  15027  resqrex  15277  sumeven  16421  ndvdsadd  16444  gcdcllem1  16533  gcdcllem3  16535  lcmftp  16670  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  divgcdcoprmex  16700  1idssfct  16714  prmodvdslcmf  17083  cshwrepswhash1  17138  xpsfrnel2  17594  xpsff1o  17597  catcone0  17719  initoeu2  18049  chnccat  18658  xpsmnd  18811  xpsgrp  19101  mulgfval  19111  gsmsymgrfix  19468  pmtr3ncom  19515  dprdfeq0  20064  gsumdixp  20363  lspcl  21040  lindsind2  21868  lindff1  21869  f1linds  21874  selvcllem5  22189  evls1maplmhm  22437  mat1dimscm  22532  tgcl  23026  elcls  23130  neiptopnei  23189  cmpfii  23466  txcnp  23677  xpstps  23867  fbun  23897  snfil  23921  filconn  23940  isufil2  23965  hauspwpwf1  24044  cnextcn  24124  ustfilxp  24270  ustuqtop4  24301  xpsxms  24591  xpsms  24592  rlmnvc  24760  nmoid  24799  xrsmopn  24870  xrhmeo  25005  cphsqrtcl  25243  iscmet3  25352  iundisj  25607  ioorinv  25635  bddiblnc  25901  dvtaylp  26430  logbid1  26830  logbchbase  26833  relogbcxpb  26849  logbmpt  26850  musum  27252  lgsmodeq  27403  lgsmulsqcoprm  27404  2lgs  27468  2sqnn0  27499  pntlem3  27670  ltsval2  27717  noxp1o  27724  cutbdaylt  27888  zsoring  28499  nb3gr2nb  29582  pthdivtx  29924  pthdlem2lem  29964  crctisclwlk  29991  wwlks  30032  wwlksonvtx  30052  wlkiswwlks2lem1  30066  wwlksnndef  30102  wwlksnfi  30103  clwlkclwwlkf1lem3  30205  clwlkclwwlkf1  30209  clwwlknnn  30232  clwwlkel  30245  wwlksext2clwwlk  30256  clwwlknonwwlknonb  30305  umgr3v3e3cycl  30383  frgrncvvdeq  30508  sspval  30923  blo3i  31002  ajfval  31009  spanval  31533  cmcmlem  31791  leopnmid  32338  csmdsymi  32534  chirredlem4  32593  sumdmdlem  32618  iundisjf  32786  iundisjfi  32995  nn0difffzod  33003  hashxpe  33006  xrpxdivcld  33109  gsumfs2d  33238  fldgensdrg  33498  lsmsnorb  33574  mxidlnzr  33652  zringfrac  33747  lactlmhm  33928  extdgval  33947  ccfldextdgrr  33966  ply1annprmidl  34001  pnfneige0  34245  rrhre  34315  esumcocn  34374  hasheuni  34379  sgon  34418  ddemeas  34530  dya2iocct  34574  dya2iocnrect  34575  eulerpartgbij  34666  eulerpartlemgs2  34674  coinflippv  34778  signstfvneq0  34863  hgt750lemb  34947  bnj1136  35289  bnj1175  35296  bnj1408  35328  fissorduni  35382  fnrelpredd  35384  fineqvnttrclselem1  35414  fineqvnttrclse  35417  unir1regs  35428  axpowg2  35440  axpowg3  35441  onvf1od  35447  vonf1wev  35448  vonf1owevOLD  35450  pthhashvtx  35475  spthcycl  35476  upgracycumgr  35500  umgracycusgr  35501  cvmsdisj  35617  mrsubvrs  35869  mppspstlem  35918  problem4  36015  climuzcnv  36018  currybi  36035  dfon2lem7  36134  imageval  36275  filnetlem2  36736  lukshef-ax2  36772  arg-ax  36773  weiunpo  36822  axtco  36828  dfttc4lem2  36886  regsfromunir1  36897  bj-andnotim  37028  bj-modalbe  37160  bj-hbs1  37294  bj-hbsb2av  37296  bj-2uplex  37504  bj-axseprep  37556  mptsnunlem  37829  onsucuni3  37858  finixpnum  38101  fin2solem  38102  matunitlindflem2  38113  poimirlem6  38122  poimirlem7  38123  poimirlem8  38124  poimirlem18  38134  poimirlem21  38137  poimirlem22  38138  poimirlem32  38148  mblfinlem3  38155  itg2addnclem2  38168  itg2addnc  38170  heiborlem3  38309  ismndo2  38370  rngomndo  38431  isfld2  38501  isfldidl  38564  dmncan2  38573  oprabbi  38657  opabbi  38661  ac6s3f  38667  relcnveq3  38823  elrelscnveq3  39123  lsat0cv  39654  djavalN  41756  djhval  42019  dochkr1  42099  dochkr1OLDN  42100  hdmap1fval  42417  lcmineqlem13  42655  fiabv  43151  mhpind  43173  pellexlem5  43407  rmyabs  43532  jm2.24  43537  islssfgi  43646  pwslnm  43668  omlimcl2  43816  onexoegt  43818  rp-oelim2  43882  oeord2lim  43883  oeord2i  43884  ensucne0OLD  44103  iscard5  44109  clrellem  44195  frege114d  44331  frege55lem1a  44439  frege70  44506  gneispace  44707  ismnushort  44874  3impexpbicom  45053  ee3bir  45076  vk15.4j  45101  onfrALTlem2  45119  ax6e2nd  45131  dfvd1impr  45149  dfvd2impr  45177  e1bir  45203  e2bir  45206  e3bir  45311  suctrALT  45398  19.21a3con13vVD  45424  3impexpbicomVD  45429  tratrbVD  45433  ssralv2VD  45438  truniALTVD  45450  trintALTVD  45452  undif3VD  45454  csbingVD  45456  onfrALTlem3VD  45459  onfrALTlem2VD  45461  onfrALTVD  45463  csbsngVD  45465  csbxpgVD  45466  csbrngVD  45468  csbunigVD  45470  csbfv12gALTVD  45471  relopabVD  45473  ax6e2ndVD  45480  2uasbanhVD  45483  vk15.4jVD  45486  sspwimp  45490  sspwimpVD  45491  sspwimpcf  45492  sspwimpcfVD  45493  suctrALTcf  45494  suctrALTcfVD  45495  suctrALT3  45496  sspwimpALT  45497  unisnALT  45498  ax6e2ndALT  45502  isosctrlem1ALT  45506  iunconnlem2  45507  prclaxpr  45558  wfaxrep  45567  supminfxrrnmpt  46042  limsuppnflem  46281  limsupubuz  46284  cncfuni  46457  stoweidlem14  46585  stoweidlem35  46606  stoweidlem57  46628  stirlinglem7  46651  fourierdlem54  46731  etransclem32  46837  subsaliuncl  46929  meadjiunlem  47036  volmea  47045  caratheodory  47099  ovnsubaddlem2  47142  hoidmvlelem5  47170  hoiqssbllem2  47194  aibandbiaiaiffb  47486  funressnvmo  47636  dfdfat2  47719  afvres  47763  ndmaovass  47797  afv2res  47830  tz6.12-afv2  47831  el1fzopredsuc  47917  fundcmpsurinjimaid  48014  iccelpart  48036  lswn0  48047  ichnfimlem  48066  prprelb  48119  indprmfz  48236  evenprm2  48333  dfnbgr6  48476  dfsclnbgr6  48477  isgrtri  48562  grlimedgclnbgr  48614  lincext1  49073  resinsnALT  49491  tposideq  49506  sepfsepc  49546  isclatd  49601  uprcl2  49807  functhincfun  50067  fullthinc  50068  setc2othin  50084