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

Theorem mpbiri 257
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbiri.min 𝜒
mpbiri.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbiri (𝜑𝜓)

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3 𝜒
21a1i 11 . 2 (𝜑𝜒)
3 mpbiri.maj . 2 (𝜑 → (𝜓𝜒))
42, 3mpbird 256 1 (𝜑𝜓)
Colors of variables: wff setvar class
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:  elimh  1081  spei  2394  nfald2  2445  nfabd2  2932  raleleqALT  3348  dedhb  3634  sbceqalOLD  3779  csbie2df  4371  ssdifeq0  4414  r19.2zb  4423  dedth  4514  pwidg  4552  elpr2OLD  4584  snidg  4592  rexreusng  4612  exsnrex  4613  ifpr  4624  rmosn  4652  rabrsn  4657  prid1g  4693  tpid1g  4702  tpid2g  4704  tpid3g  4705  pwpw0  4743  sssn  4756  elpreqpr  4794  pwsnOLD  4829  unimax  4874  intmin3  4904  eqbrtrdi  5109  al0ssb  5227  intabs  5261  pwnss  5267  difelpw  5269  rabelpw  5270  0inp0  5276  copsexgw  5398  copsexg  5399  euotd  5421  elopab  5433  elvvuni  5654  posn  5663  frsn  5665  eqrelriv  5688  relsnb  5701  relopabiALT  5722  opabid2  5727  ididg  5751  iss  5932  dfpo2  6188  ord0eln0  6305  sucidg  6329  nsuceq0  6331  funopg  6452  fn0  6548  f00  6640  f0bi  6641  f10d  6733  f1o00  6734  fo00  6735  brprcneu  6747  fvprc  6748  dffn5  6810  fsn  6989  funop  7003  funsndifnop  7005  fnsnb  7020  eufnfv  7087  f1eqcocnv  7153  f1eqcocnvOLD  7154  nfriotadw  7220  nfriotad  7224  riotaprop  7240  oprabidw  7286  oprabid  7287  elrnmpo  7388  ov6g  7414  ovelrn  7426  caovmo  7487  offn  7524  caofinvl  7541  fr3nr  7600  onprc  7605  ordeleqon  7609  onint0  7618  0elsuc  7657  onuninsuci  7662  orduninsuc  7665  ordzsl  7667  onzsl  7668  tfinds  7681  limomss  7692  limom  7703  peano5  7714  peano5OLD  7715  xpexr  7739  eqop2  7847  opreuopreu  7849  1stconst  7911  2ndconst  7912  funsssuppss  7977  dftpos3  8031  dftpos4  8032  wfrlem4OLD  8114  wfrlem14OLD  8124  oawordeulem  8347  omwordi  8364  nnmwordi  8428  riiner  8537  ecopover  8568  map0g  8630  mapsnd  8632  elixpsn  8683  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  fiprc  8789  sbthlem2  8824  sbthlem4  8826  sbthlem5  8827  nneneq  8896  findcard  8908  findcard2  8909  sdom1  8952  fineqvlem  8966  nfielex  8976  findcard2OLD  8986  elfiun  9119  marypha1lem  9122  oicl  9218  oif  9219  oion  9225  hartogslem1  9231  hartogs  9233  wemapso2  9242  card2on  9243  0wdom  9259  brwdom2  9262  inf3lem6  9321  cantnflem3  9379  cantnflem4  9380  wemapwe  9385  cnfcom  9388  tctr  9429  r1tr  9465  r1rankidb  9493  r1pw  9534  scottex  9574  scott0  9575  bnd2  9582  eldju2ndl  9613  tskwe  9639  oncard  9649  cardlim  9661  harsdom  9684  en2eleq  9695  dfac8alem  9716  cardaleph  9776  iunfictbso  9801  infmap2  9905  ackbij1lem18  9924  cff  9935  cfsuc  9944  cff1  9945  cflim2  9950  cfss  9952  sdom2en01  9989  infpssrlem4  9993  fin23lem7  10003  fin23lem11  10004  isfin2-2  10006  fin23lem26  10012  fin23lem19  10023  fin23lem17  10025  isf34lem2  10060  isf34lem4  10064  fin1a2lem6  10092  fin1a2lem10  10096  fin1a2lem12  10098  itunifn  10104  hsmexlem1  10113  axcc2lem  10123  dcomex  10134  axdc3lem4  10140  ondomon  10250  konigthlem  10255  pwcfsdom  10270  cfpwsdom  10271  axpowndlem3  10286  canth4  10334  canthnumlem  10335  canthwelem  10337  canthwe  10338  canthp1lem2  10340  pwfseqlem4  10349  pwfseqlem5  10350  gchaleph  10358  gch2  10362  winainflem  10380  0tsk  10442  rankcf  10464  tskcard  10468  gruina  10505  grutsk  10509  tskmid  10527  indpi  10594  nqereu  10616  mulcanenq  10647  recmulnq  10651  archnq  10667  ltsopr  10719  1ne0sr  10783  0idsr  10784  00sr  10786  leid  11001  lelttric  11012  divcan3  11589  lemul1a  11759  nn1suc  11925  nn0n0n1ge2b  12231  xnn0xr  12240  xnn0nemnf  12246  nn0lt10b  12312  nn0ind-raph  12350  elnn1uz2  12594  indstr2  12596  uzsupss  12609  rpnnen1lem4  12649  rpnnen1lem5  12650  xrnemnf  12782  xrnepnf  12783  mnfltxr  12792  xnn0n0n1ge2b  12796  xnn0ge0  12798  xrlttri  12802  xrlttr  12803  xrleid  12814  qbtwnxr  12863  xmullem2  12928  xlemul1a  12951  xrub  12975  reltxrnmnf  13005  ixxun  13024  xnn0xrge0  13167  fztpval  13247  fseq1p1m1  13259  elfznelfzob  13421  ltweuz  13609  fzfi  13620  fsuppmapnn0fiubex  13640  ser0f  13704  0exp  13746  faclbnd4lem1  13935  bcn1  13955  hashnemnf  13986  hashv01gt1  13987  hashsnle1  14060  hashgt12el2  14066  hashpw  14079  hashf1  14099  fz1isolem  14103  hash2prb  14114  0wrd0  14171  wrdlen1  14185  ccatvalfn  14214  eqs1  14245  wrdl1exs1  14246  swrdlen  14288  swrdwrdsymb  14303  swrdspsleq  14306  cats1un  14362  wrdind  14363  wrd2ind  14364  swrdccatin1  14366  repswsymballbi  14421  cshw1  14463  scshwfzeqfzo  14467  wrdl2exs2  14587  trclfvcotr  14648  relexp1g  14665  relexp0rel  14676  relexprelg  14677  relexpreld  14679  sqr0lem  14880  sqrtsq  14909  mptfzshft  15418  prodf1f  15532  egt2lt3  15843  0dvds  15914  nn0onn  16017  nn0o  16020  divalgmod  16043  flodddiv4  16050  bitsp1o  16068  gcddvds  16138  bezout  16179  lcmdvds  16241  rpdvds  16293  1nprm  16312  prmind2  16318  nnoddn2prmb  16442  pcpre1  16471  vdwapf  16601  vdwapid1  16604  ram0  16651  ramz  16654  prmolefac  16675  cshws0  16731  prmlem0  16735  strle1  16787  restsspw  17059  prdsdsfn  17093  imasdsfn  17142  imasaddfnlem  17156  imasvscafn  17165  xpsfrnel  17190  isacs1i  17283  cidfn  17305  fnhomeqhomf  17317  comffn  17331  isoval  17394  sscres  17452  cofucl  17519  idffth  17565  ressffth  17570  cat1lem  17727  catcoppccl  17748  catcoppcclOLD  17749  estrchomfn  17767  funcestrcsetclem4  17776  funcestrcsetclem7  17779  equivestrcsetc  17785  funcsetcestrclem4  17791  funcsetcestrclem7  17794  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlfcl  17856  curf1cl  17862  curfcl  17866  hofcl  17893  yonedainv  17915  pospo  17978  lubfun  17985  glbfun  17998  joindmss  18012  meetdmss  18026  ipopos  18169  acsficl2d  18185  dirref  18234  mgmidcl  18265  mgmlrid  18266  ielefmnd  18441  smndex1basss  18459  smndex1n0mnd  18466  cntzssv  18849  idresperm  18908  symgvalstruct  18919  symgvalstructOLD  18920  pmtrfmvdn0  18985  symggen  18993  psgnunilem1  19016  psgnprfval  19044  slwpgp  19133  frgpmhm  19286  frgpuptinv  19292  frgpup3lem  19298  gsumzoppg  19460  gsumcom2  19491  abv0  20006  rrgsupp  20475  zrhrhm  20625  psgnodpmr  20707  frlmphllem  20897  frlmphl  20898  ellspd  20919  psrvscafval  21069  psrridm  21083  ltbwe  21155  psrbag0  21180  psrbagsn  21181  subrgascl  21184  mattpostpos  21511  mavmul0  21609  mavmul0g  21610  mdet0f1o  21650  m1detdiag  21654  m2detleiblem5  21682  m2detleiblem6  21683  m2detleiblem3  21686  m2detleiblem4  21687  maducoeval2  21697  d1mat2pmat  21796  chpmat1dlem  21892  chpmat1d  21893  baspartn  22012  eltg3  22020  topnex  22054  fctop  22062  cctop  22064  discld  22148  mretopd  22151  neipeltop  22188  neitr  22239  restcls  22240  ordtbaslem  22247  ordtuni  22249  idcn  22316  cnrmi  22419  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  hauscmplem  22465  cmpfi  22467  bwth  22469  1stcrestlem  22511  disllycmp  22557  dis1stc  22558  refref  22572  kgeni  22596  1stckgenlem  22612  kqffn  22784  snfil  22923  filconn  22942  cfinfil  22952  ufileu  22978  filufint  22979  fixufil  22981  cfinufil  22987  ufilen  22989  fin1aufil  22991  fmf  23004  rnelfm  23012  flimclslem  23043  hauspwpwf1  23046  supnfcls  23079  flimfnfcls  23087  fclscmp  23089  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem1  23111  cnextrel  23122  tsmsfbas  23187  ustref  23278  trust  23289  restutop  23297  isusp  23321  xmet0  23403  imasdsf1olem  23434  blfvalps  23444  blfps  23467  blf  23468  restmetu  23632  dscmet  23634  isngp2  23659  nm0  23691  nrginvrcn  23762  nmoix  23799  qdensere  23839  iccconn  23899  iccpnfcnv  24013  xrhmeo  24015  lebnumlem3  24032  metsscmetcld  24384  bcthlem5  24397  csschl  24445  rrxmfval  24475  minveclem3b  24497  cniccbdd  24530  ovolicc2lem4  24589  iunmbl  24622  ioorinv  24645  ioorcl  24646  i1f1lem  24758  limcvallem  24940  ellimc2  24946  limccnp  24960  limccnp2  24961  limcco  24962  perfdvf  24972  recnprss  24973  fncpn  25002  dvcmulf  25014  c1lip1  25066  lhop2  25084  q1pcl  25225  r1pdeglt  25228  ply1remlem  25232  plyssc  25266  ulm0  25455  cxpeq0  25738  cxplea  25756  cxplogb  25841  asinlem  25923  isppw2  26169  muval2  26188  dchrfi  26308  dchrpt  26320  bposlem6  26342  lgsdir2lem2  26379  lgsqr  26404  gausslemma2dlem4  26422  2lgslem2  26448  2lgslem3  26457  2lgs  26460  2sqlem7  26477  2sqlem11  26482  chtppilim  26528  tgldimor  26767  tgcgr4  26796  tglnfn  26812  tglnunirn  26813  mirne  26932  mircinv  26933  perpln1  26975  perpln2  26976  lmiisolem  27061  xmstrkgc  27156  axcgrtr  27186  axsegconlem9  27196  axlowdimlem5  27217  axlowdimlem17  27229  axlowdim1  27230  uhgr0e  27344  edglnl  27416  uhgr0edgfi  27510  issubgr2  27542  subgrprop2  27544  egrsubgr  27547  0grsubgr  27548  0uhgrsubgr  27549  uhgrsubgrself  27550  nbgr0vtx  27626  nbgr1vtx  27628  nbgrssovtx  27631  nb3grprlem1  27650  uvtx01vtx  27667  cplgr1vlem  27699  cplgr1v  27700  usgrexilem  27710  wlkcomp  27900  wlk1walk  27908  wlkp1lem5  27947  uhgrwkspthlem1  28022  pthdlem1  28035  clwlkcomp  28048  lfgrn1cycl  28071  uspgrn2crct  28074  wwlksn0s  28127  umgrwwlks2on  28223  clwwlkn  28291  clwwlkn1  28306  0ewlk  28379  1ewlk  28380  0spth  28391  upgr1wlkdlem2  28411  wlk2v2e  28422  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eupth0  28479  frgr0v  28527  frgr1v  28536  1vwmgr  28541  ex-opab  28697  grpoinvf  28795  nvmid  28922  nmlnoubi  29059  hiidrcl  29358  hsn0elch  29511  shjshseli  29756  cmbr4i  29864  dfiop2  30016  kbpj  30219  nmopun  30277  adjeq0  30354  kbass2  30380  pjssdif1i  30438  pjinvari  30454  pjcmul2i  30465  pj3i  30471  stge1i  30501  stle0i  30502  sumdmdlem2  30682  dmdbr6ati  30686  dmdbr7ati  30687  rabsnel  30748  unidifsnel  30784  unidifsnne  30785  disjdifprg  30815  ofoprabco  30903  padct  30956  fpwrelmapffslem  30969  xrlelttric  30977  xnn0gt0  30994  iundisj2cnt  31022  f1ocnt  31025  fz1nnct  31026  fz1nntr  31027  hashxpe  31029  dvdszzq  31031  nn0min  31036  wrdt2ind  31127  xrge0tsmsbi  31220  locfinref  31693  dispcmp  31711  zartopn  31727  zarcmplem  31733  pstmxmet  31749  xrge0iifcnv  31785  xrge0iif1  31790  qqhre  31870  esumcl  31898  esumpr2  31935  esumpinfval  31941  esumpcvgval  31946  ofcfn  31968  pwsiga  31998  prsiga  31999  sigainb  32004  ldgenpisyslem1  32031  measiuns  32085  relfae  32115  pmeasmono  32191  sitgf  32214  eulerpartgbij  32239  sgnmulsgn  32416  sgnmulsgp  32417  signswch  32440  signslema  32441  signstlen  32446  signstfvn  32448  circlevma  32522  bnj216  32611  bnj151  32757  bnj517  32765  bnj970  32827  bnj1145  32873  bnj1498  32941  fineqvrep  32964  fineqvac  32966  0nn0m1nnn0  32971  pthhashvtx  32989  acycgr0v  33010  prclisacycgr  33013  umgracycusgr  33016  cusgracyclt3v  33018  subfacp1lem5  33046  erdszelem8  33060  kur14lem1  33068  indispconn  33096  cvmsss2  33136  satfvsuclem2  33222  satfrel  33229  satfrnmapom  33232  satfv0fun  33233  satf00  33236  satf0suclem  33237  fmlasuc0  33246  msubrn  33391  dfon2lem7  33671  ssttrcl  33701  ttrclselem2  33712  frxp2  33718  frxp3  33724  nosgnn0i  33789  nolesgn2ores  33802  nogesgn1ores  33804  nosepnelem  33809  nosepdmlem  33813  nosupbnd1lem3  33840  nosupbnd1lem5  33842  nosupbnd2lem1  33845  noinfbnd1lem3  33855  noinfbnd1lem5  33857  noinfbnd2lem1  33860  oldval  33965  made0  33984  lrrecpo  34025  brbigcup  34127  elsingles  34147  fnimage  34158  funpartlem  34171  dfrdg4  34180  imagesset  34182  altopthsn  34190  elaltxp  34204  ellines  34381  linethru  34382  rankeq1o  34400  elhf2  34404  hfninf  34415  nn0prpwlem  34438  fneref  34466  neibastop2lem  34476  limsucncmpi  34561  bj-exlimmpbir  35026  curryset  35062  bj-snglex  35090  bj-restpw  35190  bj-inftyexpidisj  35308  topdifinffinlem  35445  relowlssretop  35461  rdgeqoa  35468  finxpreclem6  35494  fvineqsneq  35510  pibt2  35515  poimirlem23  35727  poimirlem29  35733  poimirlem31  35735  volsupnfl  35749  cnambfre  35752  dvasin  35788  dvacos  35789  sdclem2  35827  sstotbnd2  35859  ssbnd  35873  ismgmOLD  35935  grpokerinj  35978  rngomndo  36020  isdrngo1  36041  ac6s6  36257  iss2  36406  cnvelrels  36540  cosselrels  36541  brssrid  36547  brcnvssrid  36552  dfdisjs5  36750  eldisjs5  36764  prtlem12  36808  riotasv2d  36898  lkrscss  37039  islshpkrN  37061  isline  37680  ispointN  37683  0psubN  37690  linepsubN  37693  atpsubN  37694  cdlemk36  38854  diafn  38975  dibfna  39095  dibvalrel  39104  dicvalrelN  39126  diclspsn  39135  dihvalrel  39220  dih1  39227  lclkrlem1  39447  lclkr  39474  mapd1o  39589  mapdin  39603  hdmapfnN  39770  hgmapfnN  39829  lcmineqlem10  39974  sticksstones9  40038  sn-iotalem  40117  repncan2  40286  sn-inelr  40356  elrfirn  40433  ismrcd1  40436  istopclsd  40438  rabren3dioph  40553  jm2.17b  40699  jm2.22  40733  jm2.23  40734  ttac  40774  pw2f1ocnv  40775  dnnumch1  40785  hbtlem5  40869  mncn0  40880  aaitgo  40903  rngunsnply  40914  ensucne0OLD  41035  clcnvlem  41120  relexp01min  41210  ntrf  41622  ssrecnpr  41815  seff  41816  sblpnf  41817  nzss  41824  dvconstbi  41841  ipo0  41956  ifr0  41957  addrfn  41979  subrfn  41980  mulvfn  41981  refsum2cnlem1  42469  ellimciota  43045  dvmptconst  43346  dvmptidg  43348  dvmulcncf  43356  dvdivcncf  43358  stoweidlem26  43457  stoweidlem50  43481  stoweidlem57  43488  aiotaval  44474  ndfatafv2nrn  44600  afv2ndefb  44603  funop1  44662  fun2dmnopgexmpl  44663  2ffzoeq  44708  iccpartiltu  44762  iccpartigtl  44763  zofldiv2ALTV  45002  evenprm2  45054  9fppr8  45077  stgoldbwt  45116  nnsum3primesle9  45134  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  tgblthelfgott  45155  isomgreqve  45165  uspgrex  45200  0mgm  45216  nnsgrpmgm  45258  c0snmhm  45361  rngchomffvalALTV  45441  funcringcsetcALTV2lem4  45485  funcringcsetclem4ALTV  45508  srhmsubc  45522  rhmsubclem1  45532  srhmsubcALTV  45540  rhmsubcALTVlem1  45550  mapsnop  45568  zlmodzxzldeplem4  45732  zofldiv2  45765  fdivval  45773  nnlog2ge0lt1  45800  dig1  45842  itcoval2  45898  itcoval3  45899  mosn  46046  mo0  46047  mof02  46054  mofeu  46063  f102g  46067  f1mo  46068  f1omo  46076  intubeu  46158  unilbeu  46159  functhinclem1  46210  fullthinc  46215  thincciso  46218  indthinc  46221  indthincALT  46222
  Copyright terms: Public domain W3C validator