MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpri Structured version   Visualization version   GIF version

Theorem biimpri 218
Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr 210. (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
StepHypRef Expression
1 biimpri.1 . . 3 (𝜑𝜓)
21bicomi 214 . 2 (𝜓𝜑)
32biimpi 206 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  mpbir  221  sylibr  224  sylbir  225  sylbbr  226  sylbb1  227  sylbb2  228  syl5bir  233  syl6ibr  242  mtbi  312  pm2.54  389  sylanbr  490  sylan2br  493  pm3.11  520  orbi2i  541  pm2.31  547  simplbi2  654  dfbi  660  sylanblrc  696  pm2.85  897  pm3.2an3  1238  syl3an1br  1362  syl3an2br  1363  syl3an3br  1364  had1  1539  nic-axALT  1596  speimfw  1873  sbbii  1884  ceqsexv2d  3229  eueq2  3362  ralun  3773  ssunieq  4438  ax6vsep  4745  opelxpi  5108  elsnxpOLD  5637  ordunidif  5732  unizlim  5803  funtpgOLD  5901  dffo2  6076  dff1o2  6099  resdif  6114  f1o00  6128  fvimacnvALT  6292  fvcofneq  6323  exfo  6333  ressnop0  6374  fsnunfv  6407  2f1fvneq  6471  ovid  6730  ovidig  6731  dfwe2  6928  onminex  6954  nnsuc  7029  1stnpr  7117  2ndnpr  7118  f1stres  7135  f2ndres  7136  1st2val  7139  2nd2val  7140  frxp  7232  soxp  7235  tz7.49  7485  elixpsn  7891  domdifsn  7987  domunsncan  8004  fineqvlem  8118  unblem4  8159  ordiso2  8364  domwdom  8423  zfreg  8444  inf3lem3  8471  trcl  8548  unir1  8620  ssrankr1  8642  pm54.43lem  8769  infxpenlem  8780  ween  8802  acni3  8814  kmlem1  8916  infdif  8975  ackbij1lem1  8986  fin23lem14  9099  fin23lem32  9110  isfin1-3  9152  axcc2lem  9202  axdc3lem2  9217  ac6c4  9247  zornn0g  9271  axdclem2  9286  rnct  9291  brdom3  9294  brdom5  9295  brdom4  9296  brdom6disj  9298  konigthlem  9334  pwcfsdom  9349  cfpwsdom  9350  alephom  9351  gruina  9584  grur1  9586  grothomex  9595  grothac  9596  nqpr  9780  axcnre  9929  axpre-sup  9934  ssxr  10051  le2tri3i  10111  muldivdir  10664  0nn0  11251  uzind4  11690  rpnnen1lem5  11762  rpnnen1lem5OLD  11768  elfz4  12277  eluzfz  12279  ssfzo12bi  12504  hashgt0elex  13129  hashxplem  13160  hashfun  13164  ishashinf  13185  ffz0iswrd  13271  wrdsymb1  13281  ccatfv0  13306  lswccats1fst  13350  ccatswrd  13394  repswfsts  13465  cshinj  13494  cshw1  13505  swrdco  13520  cotr2g  13649  xptrrel  13653  trclun  13689  resqrex  13925  pwm1geoser  14525  sumeven  15034  ndvdsadd  15058  gcdcllem1  15145  gcdcllem3  15147  lcmftp  15273  lcmfunsnlem2lem2  15276  lcmfunsnlem2  15277  lcmfun  15282  ncoprmgcdne1b  15287  coprmprod  15299  coprmproddvdslem  15300  divgcdcoprmex  15304  1idssfct  15317  prmodvdslcmf  15675  cshwrepswhash1  15733  xpsff1o  16149  initoeu2  16587  clatlem  17032  clatlubcl2  17034  clatglbcl2  17036  xpsmnd  17251  sgrp2rid2  17334  xpsgrp  17455  symg2bas  17739  symgextf  17758  gsmsymgrfix  17769  gsmsymgreqlem2  17772  pmtr3ncom  17816  odlem1  17875  gexlem1  17915  dprdfeq0  18342  gsumdixp  18530  lspcl  18895  cply1mul  19583  psgndiflemB  19865  lindfind  20074  lindsind  20075  lindsind2  20077  lindff1  20078  f1linds  20083  gsumcom3fi  20125  mat1dimscm  20200  dmatmul  20222  mdetdiag  20324  mdetunilem7  20343  mdetunilem9  20345  madurid  20369  fvmptnn04if  20573  tgcl  20684  elcls  20787  opnnei  20834  neiptopnei  20846  cnpnei  20978  cmpfii  21122  txcnp  21333  xpstps  21523  fbun  21554  isfild  21572  snfil  21578  filconn  21597  isufil2  21622  hauspwpwf1  21701  cnextcn  21781  ustfilxp  21926  ustuqtop4  21958  xpsxms  22249  xpsms  22250  rlmnvc  22417  nmoid  22456  xrsmopn  22523  xrhmeo  22653  cphsqrtcl  22892  iscmet3  22999  iundisj  23223  ioorinv  23250  plyexmo  23972  aalioulem3  23993  dvtaylp  24028  dvradcnv  24079  logtayllem  24305  logtayl  24306  logbid1  24406  logbchbase  24409  relogbcxpb  24425  logbmpt  24426  logbfval  24428  musum  24817  lgsmodeq  24967  lgsmulsqcoprm  24968  2lgs  25032  pntlem3  25198  nbupgrel  26128  nbusgrvtxm1  26168  nb3gr2nb  26173  cplgruvtxb  26198  pthdivtx  26494  pthdlem2lem  26532  crctisclwlk  26558  wwlks  26596  wspthnonp  26613  wlkiswwlks2lem1  26624  wwlksnndef  26669  clwwlksnfi  26779  clwwlksel  26780  clwwlksf1  26783  clwlksf1clwwlklem  26834  umgr3v3e3cycl  26910  frgrncvvdeq  27038  frgr2wwlkeu  27050  frrusgrord0  27061  sspval  27427  blo3i  27506  ajfval  27513  spanval  28041  cmcmlem  28299  leopnmid  28846  csmdsymi  29042  chirredlem4  29101  sumdmdlem  29126  iundisjf  29247  padct  29340  iundisjfi  29396  xrpxdivcld  29428  pnfneige0  29779  rrhre  29847  esumcocn  29923  hasheuni  29928  sgon  29968  sigapildsys  30006  ddemeas  30080  dya2iocct  30123  dya2iocnrect  30124  eulerpartgbij  30215  eulerpartlemgs2  30223  coinflippv  30326  bnj1136  30773  bnj1175  30780  bnj1408  30812  cvmsdisj  30960  mrsubvrs  31127  mppspstlem  31176  problem4  31270  climuzcnv  31273  dford5  31317  dfon2lem7  31395  sltval2  31510  nodenselem5  31548  nosino  31575  imageval  31679  filnetlem2  32016  df3nandALT1  32038  lukshef-ax2  32056  arg-ax  32057  bj-andnotim  32215  bj-modalbe  32320  bj-2uplex  32657  bj-toprntopon  32700  mptsnunlem  32817  onsucuni3  32847  finixpnum  33026  fin2solem  33027  matunitlindflem2  33038  poimirlem6  33047  poimirlem7  33048  poimirlem8  33049  poimirlem18  33059  poimirlem21  33062  poimirlem22  33063  poimirlem32  33073  mblfinlem3  33080  itg2addnclem2  33094  itg2addnc  33096  bddiblnc  33112  ftc1anclem6  33122  heiborlem3  33244  ismndo2  33305  rngomndo  33366  isfld2  33436  isfldidl  33499  dmncan2  33508  oprabbi  33602  opabbi  33606  ac6s3f  33611  lsat0cv  33800  pclfinclN  34716  docavalN  35892  djavalN  35904  dochval  36120  djhval  36167  dochexmidlem8  36236  dochkr1  36247  dochkr1OLDN  36248  hdmap1fval  36566  pellexlem5  36877  rmyabs  37005  jm2.24  37010  islssfgi  37122  pwslnm  37144  dgraaub  37199  clrellem  37410  frege114d  37531  frege55lem1a  37642  frege70  37709  gneispace  37914  3impexpbicom  38167  ee3bir  38191  vk15.4j  38216  onfrALTlem2  38243  ax6e2nd  38256  dfvd1impr  38274  dfvd2impr  38311  e1bir  38337  e2bir  38340  e3bir  38448  suctrALT  38544  19.21a3con13vVD  38570  3impexpbicomVD  38575  tratrbVD  38580  ssralv2VD  38585  truniALTVD  38597  trintALTVD  38599  undif3VD  38601  onfrALTlem3VD  38606  onfrALTlem2VD  38608  onfrALTVD  38610  relopabVD  38620  ax6e2ndVD  38627  2uasbanhVD  38630  vk15.4jVD  38633  sspwimp  38637  sspwimpVD  38638  sspwimpcf  38639  sspwimpcfVD  38640  suctrALTcf  38641  suctrALTcfVD  38642  suctrALT3  38643  sspwimpALT  38644  unisnALT  38645  ax6e2ndALT  38649  isosctrlem1ALT  38653  iunconnlem2  38654  limsuppnflem  39346  limsupubuz  39349  cncfuni  39403  iblcncfioo  39501  stoweidlem14  39538  stoweidlem17  39541  stoweidlem35  39559  stoweidlem57  39581  stirlinglem7  39604  stirlinglem10  39607  fourierdlem54  39684  fourierdlem62  39692  fourierdlem63  39693  fourierdlem65  39695  fourierdlem73  39703  fourierdlem80  39710  fourierdlem82  39712  fourierdlem101  39731  etransclem32  39790  ioorrnopnxr  39834  subsaliuncl  39883  meadjiunlem  39989  ismeannd  39991  voliunsge0lem  39996  volmea  39998  caratheodory  40049  ovnsubaddlem2  40092  hoidmvlelem5  40120  hoiqssbllem2  40144  iinhoiicc  40195  aibandbiaiaiffb  40366  dfdfat2  40515  afvres  40556  tz6.12-afv  40557  ndmaovass  40590  el1fzopredsuc  40632  fzoopth  40634  iccpartiltu  40656  iccelpart  40667  lswn0  40678  ccatpfx  40708  evenprm2  40922  lincext1  41531
  Copyright terms: Public domain W3C validator