Theorem biimpri 227

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mpbir  230  sylibr  233  sylbir  234  sylbbr  235  sylbb1  236  sylbb2  237  syl5bir  242  syl6ibr  251  mtbi  321  sylnib  327  simplbi2  500  sylanbr  581  sylan2br  594  pm2.54  848  orbi2i  909  pm2.31  919  pm2.85  929  pm3.11  989  syl3an1br  1404  syl3an2br  1405  syl3an3br  1406  had1  1606  nic-axALT  1678  speimfw  1968  sbbii  2080  hbsbw  2171  mobii  2548  mo4  2566  nfabdwOLD  2930  r19.30  3265  r19.30OLD  3266  ceqsexv2d  3471  eueq2  3640  ralun  4122  ssunieq  4873  ax6vsep  5222  opelxpi  5617  ordunidif  6299  unizlim  6368  dffo2  6676  dff1o2  6705  resdif  6720  f1o00  6734  fvimacnvALT  6916  fvcofneq  6951  exfo  6963  ressnop0  7007  fsnunfv  7041  ovid  7392  ovidig  7393  dfwe2  7602  onminex  7629  nnsuc  7705  1stnpr  7808  2ndnpr  7809  f1stres  7828  f2ndres  7829  1st2val  7832  2nd2val  7833  frxp  7938  soxp  7941  fprlem1  8087  tz7.49  8246  elixpsn  8683  domdifsn  8795  domunsncan  8812  unfi  8917  cnvfi  8924  fineqvlem  8966  unblem4  8999  ordiso2  9204  zfreg  9284  inf3lem3  9318  trcl  9417  unir1  9502  ssrankr1  9524  djuunxp  9610  pm54.43lem  9689  infxpenlem  9700  ween  9722  acni3  9734  kmlem1  9837  infdif  9896  ackbij1lem1  9907  fin23lem32  10031  isfin1-3  10073  axdc3lem2  10138  ac6c4  10168  zornn0g  10192  axdclem2  10207  rnct  10212  brdom3  10215  brdom5  10216  brdom4  10217  brdom6disj  10219  konigthlem  10255  pwcfsdom  10270  cfpwsdom  10271  alephom  10272  gruina  10505  grur1  10507  grothomex  10516  grothac  10517  nqpr  10701  axcnre  10851  axpre-sup  10856  ssxr  10975  le2tri3i  11035  muldivdir  11598  0nn0  12178  uzind4  12575  rpnnen1lem5  12650  elfz4  13178  eluzfz  13180  ssfzo12bi  13410  hashgt0elex  14044  hashgt23el  14067  hashxplem  14076  hashfun  14080  ishashinf  14105  wrdsymb1  14184  ccatfv0  14216  lswccats1fst  14273  ccatswrd  14309  ccatpfx  14342  splfv1  14396  repswfsts  14422  cshinj  14452  swrdco  14478  cotr2g  14615  trclun  14653  resqrex  14890  sumeven  16024  ndvdsadd  16047  gcdcllem1  16134  gcdcllem3  16136  lcmftp  16269  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  lcmfun  16278  coprmprod  16294  coprmproddvdslem  16295  divgcdcoprmex  16299  1idssfct  16313  prmodvdslcmf  16676  cshwrepswhash1  16732  xpsfrnel2  17192  xpsff1o  17195  catcone0  17313  initoeu2  17647  clatlem  18135  clatlubcl2  18137  clatglbcl2  18139  xpsmnd  18340  xpsgrp  18609  mulgfval  18617  gsmsymgrfix  18951  pmtr3ncom  18998  gsumcom3fi  19495  dprdfeq0  19540  gsumdixp  19763  lspcl  20153  lindfind  20933  lindsind  20934  lindsind2  20936  lindff1  20937  f1linds  20942  mat1dimscm  21532  mdetunilem7  21675  fvmptnn04if  21906  tgcl  22027  elcls  22132  opnnei  22179  neiptopnei  22191  cnpnei  22323  cmpfii  22468  txcnp  22679  xpstps  22869  fbun  22899  isfild  22917  snfil  22923  filconn  22942  isufil2  22967  hauspwpwf1  23046  cnextcn  23126  ustfilxp  23272  ustuqtop4  23304  xpsxms  23596  xpsms  23597  rlmnvc  23773  nmoid  23812  xrsmopn  23881  xrhmeo  24015  cphsqrtcl  24253  iscmet3  24362  iundisj  24617  ioorinv  24645  bddiblnc  24911  dvtaylp  25434  logbid1  25823  logbchbase  25826  relogbcxpb  25842  logbmpt  25843  logbfval  25845  musum  26245  lgsmodeq  26395  lgsmulsqcoprm  26396  2lgs  26460  2sqnn0  26491  pntlem3  26662  nbupgrel  27615  nbusgrvtxm1  27649  nb3gr2nb  27654  pthdivtx  27998  pthdlem2lem  28036  crctisclwlk  28063  wwlks  28101  wwlksonvtx  28121  wspthnonp  28125  wlkiswwlks2lem1  28135  wwlksnndef  28171  wwlksnfi  28172  clwlkclwwlkf1lem3  28271  clwlkclwwlkf1  28275  clwwlknnn  28298  clwwlkel  28311  clwwlkf1  28314  wwlksext2clwwlk  28322  clwwlknonwwlknonb  28371  umgr3v3e3cycl  28449  frgrncvvdeq  28574  sspval  28986  blo3i  29065  ajfval  29072  spanval  29596  cmcmlem  29854  leopnmid  30401  csmdsymi  30597  chirredlem4  30656  sumdmdlem  30681  iundisjf  30829  padct  30956  iundisjfi  31019  hashxpe  31029  fprodex01  31041  xrpxdivcld  31111  lsmsnorb  31481  mxidlnzr  31541  extdgval  31631  ccfldextdgrr  31644  pnfneige0  31803  rrhre  31871  esumcocn  31948  hasheuni  31953  sgon  31992  sigapildsys  32030  ddemeas  32104  dya2iocct  32147  dya2iocnrect  32148  eulerpartgbij  32239  eulerpartlemgs2  32247  coinflippv  32350  signstfvneq0  32451  hgt750lemb  32536  bnj1136  32877  bnj1175  32884  bnj1408  32916  fnrelpredd  32961  pthhashvtx  32989  spthcycl  32991  upgracycumgr  33015  umgracycusgr  33016  cvmsdisj  33132  mrsubvrs  33384  mppspstlem  33433  problem4  33526  climuzcnv  33529  dford5  33573  dfon2lem7  33671  frxp2  33718  sltval2  33786  noxp1o  33793  conway  33920  scutbdaylt  33939  imageval  34159  filnetlem2  34495  df3nandALT1  34515  lukshef-ax2  34531  arg-ax  34532  bj-andnotim  34697  bj-modalbe  34797  bj-hbs1  34921  bj-hbsb2av  34923  bj-2uplex  35139  mptsnunlem  35436  onsucuni3  35465  fvineqsneq  35510  finixpnum  35689  fin2solem  35690  matunitlindflem2  35701  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem32  35736  mblfinlem3  35743  itg2addnclem2  35756  itg2addnc  35758  ftc1anclem6  35782  heiborlem3  35898  ismndo2  35959  rngomndo  36020  isfld2  36090  isfldidl  36153  dmncan2  36162  oprabbi  36246  opabbi  36250  ac6s3f  36256  relcnveq3  36383  elrelscnveq3  36536  lsat0cv  36974  pclfinclN  37891  docavalN  39064  djavalN  39076  dochval  39292  djhval  39339  dochexmidlem8  39408  dochkr1  39419  dochkr1OLDN  39420  hdmap1fval  39737  lcmineqlem13  39977  selvval2lem5  40155  mhpind  40206  pellexlem5  40571  rmyabs  40696  jm2.24  40701  islssfgi  40813  pwslnm  40835  dgraaub  40889  ensucne0OLD  41035  iscard5  41039  clrellem  41119  frege114d  41255  frege55lem1a  41363  frege70  41430  gneispace  41633  ismnushort  41808  3impexpbicom  41988  ee3bir  42012  vk15.4j  42037  onfrALTlem2  42055  ax6e2nd  42067  dfvd1impr  42085  dfvd2impr  42113  e1bir  42139  e2bir  42142  e3bir  42248  suctrALT  42335  19.21a3con13vVD  42361  3impexpbicomVD  42366  tratrbVD  42370  ssralv2VD  42375  truniALTVD  42387  trintALTVD  42389  undif3VD  42391  onfrALTlem3VD  42396  onfrALTlem2VD  42398  onfrALTVD  42400  relopabVD  42410  ax6e2ndVD  42417  2uasbanhVD  42420  vk15.4jVD  42423  sspwimp  42427  sspwimpVD  42428  sspwimpcf  42429  sspwimpcfVD  42430  suctrALTcf  42431  suctrALTcfVD  42432  suctrALT3  42433  sspwimpALT  42434  unisnALT  42435  ax6e2ndALT  42439  isosctrlem1ALT  42443  iunconnlem2  42444  supminfxrrnmpt  42901  limsuppnflem  43141  limsupubuz  43144  cncfuni  43317  iblcncfioo  43409  stoweidlem14  43445  stoweidlem17  43448  stoweidlem35  43466  stoweidlem57  43488  stirlinglem7  43511  stirlinglem10  43514  fourierdlem54  43591  fourierdlem62  43599  fourierdlem63  43600  fourierdlem65  43602  fourierdlem73  43610  fourierdlem80  43617  fourierdlem82  43619  fourierdlem101  43638  etransclem32  43697  ioorrnopnxr  43738  subsaliuncl  43787  meadjiunlem  43893  ismeannd  43895  voliunsge0lem  43900  volmea  43902  caratheodory  43956  ovnsubaddlem2  43999  hoidmvlelem5  44027  hoiqssbllem2  44051  iinhoiicc  44102  aibandbiaiaiffb  44277  funressnvmo  44426  dfdfat2  44507  afvres  44551  tz6.12-afv  44552  ndmaovass  44585  afv2res  44618  tz6.12-afv2  44619  el1fzopredsuc  44705  fzoopth  44707  fundcmpsurinjimaid  44751  iccpartiltu  44762  iccelpart  44773  lswn0  44784  ichnfimlem  44803  prprelb  44856  evenprm2  45054  lincext1  45683  sepfsepc  46109  isclatd  46157  intubeu  46158  unilbeu  46159  fullthinc  46215  setc2othin  46225