Theorem biimpri 231

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mpbir  234  sylibr  237  sylbir  238  sylbbr  239  sylbb1  240  sylbb2  241  biimtrrid  246  imbitrrdi  255  mtbi  325  sylnib  331  simplbi2  506  biranri  511  bilanri  512  sylanbr  594  sylan2br  607  pm2.54  866  orbi2i  926  pm2.31  936  pm2.85  946  pm3.11  1008  syl3an1br  1433  syl3an2br  1434  syl3an3br  1435  had1OLD  1635  nic-axALT  1707  speimfw  1996  sbbii  2113  mo4  2591  r19.30  3129  eueq2  3668  ralun  4144  ssunieq  4904  replem  5243  ax6vsep  5260  opelxpi  5692  ordunidif  6408  unizlim  6482  dffo2  6793  dff1o2  6823  resdif  6839  fvimacnvALT  7049  fvcofneq  7086  exfo  7098  ressnop0  7150  fsnunfv  7185  2f1fvneq  7257  ovid  7554  ovidig  7555  uniex2  7739  dfwe2  7773  dford5  7783  onminex  7801  nnsuc  7880  1stnpr  7990  2ndnpr  7991  1st2val  8014  2nd2val  8015  frxp  8124  soxp  8127  fprlem1  8299  tz7.49  8434  domdifsn  9058  domunsncan  9075  unfi  9165  cnvfi  9170  fineqvlem  9236  unblem4  9265  zfreg  9568  elirrvOLD  9570  inf3lem3  9609  unir1  9795  ssrankr1  9817  djuunxp  9926  pm54.43lem  10005  infxpenlem  10016  ween  10038  acni3  10050  kmlem1  10153  infdif  10210  ackbij1lem1  10221  fin23lem32  10346  isfin1-3  10388  axdc3lem2  10453  ac6c4  10483  zornn0g  10507  axdclem2  10522  rnct  10528  brdom3  10531  brdom5  10532  brdom4  10533  brdom6disj  10535  konigthlem  10577  pwcfsdom  10592  cfpwsdom  10593  alephom  10594  gruina  10827  grur1  10829  grothac  10839  nqpr  11023  axcnre  11173  ssxr  11303  le2tri3i  11364  muldivdir  11931  0nn0  12543  uzind4  12955  rpnnen1lem5  13031  elfz4  13571  eluzfz  13573  ssfzo12bi  13817  fzoopth  13818  hashgt0elex  14465  hashgt23el  14489  hashxplem  14498  hashfun  14502  ishashinf  14528  wrdsymb1  14618  ccatfv0  14649  lswccats1fst  14703  ccatswrd  14738  ccatpfx  14770  splfv1  14824  cshinj  14882  swrdco  14908  cotr2g  15049  trclun  15087  resqrex  15337  sumeven  16477  ndvdsadd  16500  gcdcllem1  16589  gcdcllem3  16591  lcmftp  16726  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  divgcdcoprmex  16756  1idssfct  16770  prmodvdslcmf  17139  cshwrepswhash1  17194  xpsfrnel2  17650  xpsff1o  17653  catcone0  17775  initoeu2  18105  chnccat  18714  xpsmnd  18884  xpsgrp  19182  mulgfval  19192  gsmsymgrfix  19555  pmtr3ncom  19602  dprdfeq0  20151  gsumdixp  20459  lspcl  21160  lindsind2  22032  lindff1  22033  f1linds  22038  selvcllem5  22355  evls1maplmhm  22602  mat1dimscm  22697  matunitlindflem2  22902  tgcl  23194  elcls  23298  neiptopnei  23357  cmpfii  23634  txcnp  23846  xpstps  24036  fbun  24066  snfil  24090  filconn  24109  isufil2  24134  hauspwpwf1  24213  cnextcn  24293  ustfilxp  24439  ustuqtop4  24470  xpsxms  24760  xpsms  24761  rlmnvc  24929  nmoid  24968  xrsmopn  25039  xrhmeo  25174  cphsqrtcl  25412  iscmet3  25521  iundisj  25776  ioorinv  25804  bddiblnc  26069  dvtaylp  26606  logbid1  27005  logbchbase  27008  relogbcxpb  27024  logbmpt  27025  musum  27427  lgsmodeq  27578  lgsmulsqcoprm  27579  2lgs  27643  2sqnn0  27674  pntlem3  27845  ltsval2  27892  noxp1o  27899  cutbdaylt  28063  zsoring  28674  nb3gr2nb  29844  pthdivtx  30191  pthhashvtx  30194  pthdlem2lem  30232  crctisclwlk  30260  spthcycl  30271  wwlks  30303  wwlksonvtx  30323  wlkiswwlks2lem1  30337  wwlksnndef  30373  wwlksnfi  30374  clwlkclwwlkf1lem3  30476  clwlkclwwlkf1  30480  clwwlknnn  30503  clwwlkel  30516  wwlksext2clwwlk  30527  clwwlknonwwlknonb  30576  umgr3v3e3cycl  30664  frgrncvvdeq  30789  sspval  31204  blo3i  31283  ajfval  31290  spanval  31814  cmcmlem  32072  leopnmid  32619  csmdsymi  32815  chirredlem4  32874  sumdmdlem  32899  iundisjf  33062  iundisjfi  33267  nn0difffzod  33275  hashxpe  33278  xrpxdivcld  33380  gsumfs2d  33501  fldgensdrg  33755  lsmsnorb  33824  mxidlnzr  33870  zringfrac  33964  lactlmhm  34144  extdgval  34163  ccfldextdgrr  34182  ply1annprmidl  34217  pnfneige0  34461  rrhre  34531  esumcocn  34590  hasheuni  34595  sgon  34634  ddemeas  34747  dya2iocct  34791  dya2iocnrect  34792  eulerpartgbij  34883  eulerpartlemgs2  34891  coinflippv  34995  signstfvneq0  35080  hgt750lemb  35164  bnj1136  35506  bnj1175  35513  bnj1408  35545  fissorduni  35594  fnrelpredd  35596  dfscott3  35626  fineqvnttrclselem1  35647  fineqvnttrclse  35650  unir1regs  35661  axpowg2  35673  axpowg3  35674  onvf1od  35704  vonf1wev  35705  vonf1owevOLD  35707  upgracycumgr  35732  umgracycusgr  35733  cvmsdisj  35849  mrsubvrs  36101  mppspstlem  36150  problem4  36247  climuzcnv  36250  currybi  36267  dfon2lem7  36366  imageval  36507  filnetlem2  36998  lukshef-ax2  37034  arg-ax  37035  weiunpo  37084  axtco  37090  dfttc4lem2  37148  regsfromunir1  37159  bj-andnotim  37289  bj-modalbe  37421  bj-hbs1  37555  bj-hbsb2av  37557  bj-2uplex  37766  bj-axseprep  37819  mptsnunlem  38092  onsucuni3  38121  finixpnum  38359  fin2solem  38360  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem18  38387  poimirlem21  38390  poimirlem22  38391  poimirlem32  38401  mblfinlem3  38408  itg2addnclem2  38421  itg2addnc  38423  heiborlem3  38563  ismndo2  38624  rngomndo  38685  isfld2  38755  isfldidl  38818  dmncan2  38827  oprabbi  38909  opabbi  38913  ac6s3f  38919  relcnveq3  39075  elrelscnveq3  39375  lsat0cv  39906  djavalN  42008  djhval  42271  dochkr1  42351  dochkr1OLDN  42352  hdmap1fval  42669  lcmineqlem13  42907  fiabv  43418  mhpind  43440  pellexlem5  43674  rmyabs  43799  jm2.24  43804  islssfgi  43913  pwslnm  43935  omlimcl2  44083  onexoegt  44085  rp-oelim2  44149  oeord2lim  44150  oeord2i  44151  ensucne0OLD  44370  iscard5  44376  clrellem  44462  frege114d  44598  frege55lem1a  44706  frege70  44773  gneispace  44974  ismnushort  45125  3impexpbicom  45303  ee3bir  45326  vk15.4j  45351  onfrALTlem2  45369  ax6e2nd  45381  dfvd1impr  45399  dfvd2impr  45427  e1bir  45453  e2bir  45456  e3bir  45561  suctrALT  45648  19.21a3con13vVD  45674  3impexpbicomVD  45679  tratrbVD  45683  ssralv2VD  45688  truniALTVD  45700  trintALTVD  45702  undif3VD  45704  csbingVD  45706  onfrALTlem3VD  45709  onfrALTlem2VD  45711  onfrALTVD  45713  csbsngVD  45715  csbxpgVD  45716  csbrngVD  45718  csbunigVD  45720  csbfv12gALTVD  45721  relopabVD  45723  ax6e2ndVD  45730  2uasbanhVD  45733  vk15.4jVD  45736  sspwimp  45740  sspwimpVD  45741  sspwimpcf  45742  sspwimpcfVD  45743  suctrALTcf  45744  suctrALTcfVD  45745  suctrALT3  45746  sspwimpALT  45747  unisnALT  45748  ax6e2ndALT  45752  isosctrlem1ALT  45756  iunconnlem2  45757  prclaxpr  45808  wfaxrep  45817  supminfxrrnmpt  46299  limsuppnflem  46538  limsupubuz  46541  cncfuni  46714  stoweidlem14  46842  stoweidlem35  46863  stoweidlem57  46885  stirlinglem7  46908  fourierdlem54  46988  etransclem32  47094  subsaliuncl  47186  meadjiunlem  47293  volmea  47302  caratheodory  47356  ovnsubaddlem2  47399  hoidmvlelem5  47427  hoiqssbllem2  47451  aibandbiaiaiffb  47783  funressnvmo  47933  dfdfat2  48016  afvres  48060  ndmaovass  48094  afv2res  48127  tz6.12-afv2  48128  el1fzopredsuc  48214  fundcmpsurinjimaid  48311  iccelpart  48333  lswn0  48344  ichnfimlem  48363  prprelb  48416  indprmfz  48533  evenprm2  48630  dfnbgr6  48773  dfsclnbgr6  48774  isgrtri  48859  grlimedgclnbgr  48911  idomcanr  49263  lincext1  49384  resinsnALT  49799  tposideq  49814  sepfsepc  49854  isclatd  49909  uprcl2  50115  functhincfun  50375  fullthinc  50376  setc2othin  50392  alsralrex  50741