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

Theorem mpbir 221
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)
Hypotheses
Ref Expression
mpbir.min 𝜓
mpbir.maj (𝜑𝜓)
Assertion
Ref Expression
mpbir 𝜑

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2 𝜓
2 mpbir.maj . . 3 (𝜑𝜓)
32biimpri 218 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  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:  pm5.74ri  261  con4bii  311  orri  391  imorri  430  imnani  439  mpbir2an  954  mpbir3an  1242  xorexmid  1477  tru  1484  had1  1539  nic-mpALT  1594  nic-ax  1595  nic-axALT  1596  nfi  1711  mpgbir  1723  nfxfr  1776  19.35ri  1804  nfxfrOLD  1834  ax5e  1838  ax6ev  1887  exanOLDOLD  2166  ax13  2248  ax13ALT  2304  euequ1  2475  moanmo  2531  axi12  2599  axext2  2602  eqeltri  2694  nfcxfr  2759  neir  2793  neirr  2799  eqnetri  2860  nelir  2896  mprgbir  2923  vex  3193  issetri  3200  moeq  3369  rmoeq  3392  cdeqi  3407  eqsstri  3620  3sstr4i  3629  rabnc  3942  tpid1  4280  tpid2  4281  pwv  4408  uni0  4438  int0  4462  eqbrtri  4644  tr0  4734  trv  4735  zfrep4  4749  zfnuleu  4756  axnulALT  4757  0ex  4760  inex1  4769  elpwi2  4799  0elpw  4804  axpow2  4815  axpow3  4816  pwex  4818  dvdemo1  4873  zfpair2  4878  exss  4902  opwo0id  4931  moop2  4936  pwundif  4991  po0  5020  epse  5067  relsnop  5195  relxp  5198  rel0  5214  relopabi  5215  relopabiALT  5216  eliunxp  5229  opeliunxp2  5230  dmi  5310  xpidtr  5487  xpima  5545  cnvcnv  5555  cnvcnvOLD  5556  dmsn0  5571  cnvsn0  5572  0elon  5747  funmpt  5894  funmpt2  5895  funcnv0  5923  isarep2  5946  fresaunres2  6043  f0  6053  f10  6136  f10d  6137  f1o00  6138  f1oi  6141  f1osn  6143  brprcneu  6151  opabiotafun  6226  fvopab3ig  6245  opabex  6448  mptexgf  6450  eufnfv  6456  isof1oopb  6540  canth  6573  ncanth  6574  mpt2fun  6727  reldmmpt2  6736  ovid  6742  ovidig  6743  ovidi  6744  ovig  6747  ov3  6762  caovmo  6836  relmptopab  6848  porpss  6906  uniex2  6917  snnexOLD  6931  tfinds2  7025  finds  7054  finds2  7056  oprabex  7116  oprabex3  7117  f1stres  7150  f2ndres  7151  relmpt2opab  7219  opeliunxp2f  7296  tpos0  7342  wfrrel  7380  wfrlem14  7388  wfrlem16  7390  issmo  7405  tfrlem6  7438  tfrlem8  7440  tfrlem16  7449  tfr1a  7450  tfr1  7453  tz7.44lem1  7461  seqomlem2  7506  seqomlem3  7507  seqomlem4  7508  fnseqom  7510  0lt1o  7544  0we1  7546  eqer  7737  eqerOLD  7738  ecopover  7811  ecopoverOLD  7812  mapsnf1o3  7866  ssdomg  7961  ensn1  7980  snfi  7998  xpcomf1o  8009  map2xp  8090  limensuci  8096  sdom1  8120  unblem4  8175  fidomdm  8203  marypha1lem  8299  hartogslem1  8407  hartogs  8409  card2on  8419  ruALT  8468  inf2  8480  inf3lem6  8490  infeq5i  8493  zfinf2  8499  cantnflt  8529  cnfcom  8557  trcl  8564  tz9.1c  8566  tc2  8578  r1funlim  8589  r1fnon  8590  karden  8718  tskwe  8736  cardprclem  8765  pm54.43  8786  r0weon  8795  iunmapdisj  8806  alephfnon  8848  alephfplem4  8890  alephfp  8891  alephval3  8893  aceq3lem  8903  kmlem2  8933  cda1dif  8958  ackbij1  9020  ackbij2lem2  9022  ackbij2  9025  infpssrlem3  9087  hsmexlem4  9211  hsmexlem5  9212  axdc3lem4  9235  ac2  9243  axac3  9246  ac6  9262  axdclem2  9302  dmct  9306  ondomon  9345  alephsucpw  9352  pwcfsdom  9365  cfpwsdom  9366  smobeth  9368  axpowndlem3  9381  zfcndun  9397  zfcndpow  9398  zfcndinf  9400  zfcndac  9401  wunex2  9520  uniwun  9522  wuncval2  9529  grur1  9602  axgroth5  9606  axgroth2  9607  axgroth6  9610  axgroth3  9613  grothtsk  9617  inaprc  9618  ltsopi  9670  dmaddpi  9672  dmmulpi  9673  1lt2pi  9687  nqerf  9712  addnqf  9730  mulnqf  9731  1lt2nq  9755  m1p1sr  9873  m1m1sr  9874  0lt1sr  9876  axaddf  9926  axmulf  9927  ax1cn  9930  subaddrii  10330  ixi  10616  recgt0ii  10889  nn1suc  11001  neg1lt0  11087  4d2e2  11144  arch  11249  un0mulcl  11287  pnf0xnn0  11330  3halfnz  11416  nummac  11518  uzf  11650  indstr  11716  mnfltpnf  11920  ixxf  12143  ioof  12229  fzf  12288  0nelfz1  12318  fzp1disj  12357  fzp1nel  12381  fzof  12424  om2uzrani  12707  om2uzf1oi  12708  uzrdglem  12712  uzrdgfni  12713  uzrdg0i  12714  ltwenn  12717  hashgf1o  12726  axdc4uzlem  12738  sq0  12911  irec  12920  facmapnn  13028  hashkf  13075  hashfxnn0  13080  hashf  13081  hashfOLD  13082  hash0  13114  prhash2ex  13143  hashsslei  13169  hashxplem  13176  hashbclem  13190  hashf1lem1  13193  wrdexg  13270  s1dm  13343  revs1  13467  0csh0  13492  cshw1  13521  cats1fvn  13556  s2dm  13587  funcnvs1  13609  relexp0g  13712  relexpsucnnr  13715  dfrtrclrec2  13747  rtrclreclem1  13748  rtrclreclem2  13749  rtrclreclem4  13751  dfrtrcl2  13752  climmo  14238  fsumcom2  14452  fsumcom2OLD  14453  ackbijnn  14504  incexclem  14512  infcvgaux1i  14533  fprodcom2  14658  fprodcom2OLD  14659  fprodn0f  14666  fprodge0  14668  fprodge1  14670  bpolylem  14723  bpoly3  14733  bpoly4  14734  efcvgfsum  14760  cos1bnd  14861  cos2bnd  14862  znnen  14885  qnnen  14886  aleph1re  14918  3dvds  14995  3dvdsOLD  14996  n2dvdsm1  15048  n2dvds3  15050  divalglem5  15063  flodddiv4  15080  bitsf  15092  sadcaddlem  15122  sadadd2lem  15124  sadadd3  15126  sadaddlem  15131  lcmf0  15290  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  coprmprod  15318  coprmproddvdslem  15319  2prm  15348  3lcm2e6  15383  phicl2  15416  pockthi  15554  unbenlem  15555  prmrec  15569  vdwlem13  15640  vdwnn  15645  ramcl2  15663  prmgapprmo  15709  mod2xnegi  15718  modsubi  15719  prmo4  15778  prmo5  15779  prmo6  15780  structcnvcnv  15813  setsres  15841  strfv  15847  strlemor1OLD  15909  strleun  15912  0rest  16030  firest  16033  restid  16034  prdsval  16055  prdsbas  16057  prdsplusg  16058  prdsmulr  16059  prdsvsca  16060  prdsds  16064  imasaddfnlem  16128  imasvscafn  16137  oppchomfval  16314  oppcbas  16318  2oppchomf  16324  rescbas  16429  rescco  16432  rescabs  16433  0ssc  16437  0subcat  16438  idfucl  16481  wunnat  16556  homarel  16626  dmaf  16639  cdaf  16640  catcfuccl  16699  relxpchom  16761  catcxpccl  16787  oppchofcl  16840  oyoncl  16850  odubas  17073  letsr  17167  mgmidmo  17199  releqg  17581  ga0  17671  oppglem  17720  psgnunilem3  17856  psgnunilem4  17857  pmtrsn  17879  efgval  18070  efger  18071  efgsp1  18090  efgsfo  18092  efgredleme  18096  efgredlem  18100  efgred  18101  cygctb  18233  gsum2d2lem  18312  gsum2d2  18313  gsumcom2  18314  dprd2d2  18383  pgpfaclem1  18420  mgplem  18434  mgpress  18440  opprlem  18568  reldvdsr  18584  00lsp  18921  sralem  19117  srasca  19121  sravsca  19122  psrvscafval  19330  opsrbaslem  19417  opsrbaslemOLD  19418  psrbag0  19434  00ply1bas  19550  ply1plusgfvi  19552  cnfldfun  19698  cnfldfunALT  19699  xrsmgm  19721  zlmsca  19809  znbaslem  19826  znbaslemOLD  19827  resubdrg  19894  ocvfval  19950  ocv0  19961  cssval  19966  thlbas  19980  thlle  19981  islinds2  20092  matsca  20161  m2detleib  20377  tgdom  20722  tgidm  20724  indistps2ALT  20758  restbas  20902  resttopon  20905  rest0  20913  leordtval2  20956  iocpnfordt  20959  icomnfordt  20960  iooordt  20961  cnpfval  20978  iscnp2  20983  ist1-3  21093  1stcfb  21188  islly2  21227  comppfsc  21275  1stckgen  21297  ptbasfi  21324  xkotf  21328  dfac14  21361  opnfbas  21586  hauspwpwf1  21731  alexsubALTlem4  21794  alexsubALT  21795  ptcmplem5  21800  cnextrel  21807  ust0  21963  tuslem  22011  0met  22111  prdsdsf  22112  prdsxmetlem  22113  prdsmet  22115  setsmsbas  22220  setsmsds  22221  prdsbl  22236  tngds  22392  qtopbaslem  22502  xrtgioo  22549  xrsdsre  22553  zcld  22556  recld2  22557  sszcld  22560  reperflem  22561  retopconn  22572  iccpnfcnv  22683  bndth  22697  ishtpy  22711  nmoleub2lem2  22856  zclmncvs  22888  recmet  23060  resscdrg  23094  ishl2  23106  recms  23108  volf  23237  iundisj2  23257  volsup  23264  icombl  23272  ioombl  23273  ismbf3d  23361  0plef  23379  0pledm  23380  itg1ge0  23393  mbfi1fseqlem5  23426  itg2addlem  23465  iblcnlem1  23494  reldv  23574  limciun  23598  dvexp  23656  dveflem  23680  lhop1lem  23714  lhop  23717  elply2  23890  elplyd  23896  ply1term  23898  ply0  23902  plymullem  23910  qaa  24016  pserulm  24114  pserdvlem2  24120  efcn  24135  sincosq1lem  24187  tangtx  24195  sincos4thpi  24203  sincos6thpi  24205  pige3  24207  efif1olem4  24229  logf1o  24249  relogf1o  24251  log1  24270  loge  24271  relogiso  24282  dvrelog  24317  relogcn  24318  logcn  24327  cxpcn3  24423  resqrtcn  24424  leibpi  24603  log2ublem1  24607  birthday  24615  emcllem5  24660  harmonicbnd  24664  harmonicbnd2  24665  emgt0  24667  harmonicbnd3  24668  lgamgulm2  24696  lgamcvglem  24700  gamf  24703  ppiltx  24837  ppiublem1  24861  ppiub  24863  bclbnd  24939  bpos1lem  24941  bposlem8  24950  lgsquadlem2  25040  2sqlem9  25086  2sqlem10  25087  chebbnd1  25095  selberg2lem  25173  pntrsumo1  25188  selbergsb  25198  pntpbnd  25211  istrkg2ld  25293  tgcgr4  25360  ttgval  25689  ttglem  25690  cchhllem  25701  ax5seglem7  25749  axlowdimlem4  25759  axlowdimlem6  25761  axlowdimlem7  25762  axlowdimlem10  25765  axlowdimlem13  25768  axlowdimlem16  25771  uhgr0e  25896  uhgr0  25898  upgrbi  25918  umgrbi  25925  usgr0  26062  lfuhgr1v0e  26073  usgrexmpllem  26079  usgrexmpl  26082  griedg0prc  26083  cplgr0  26242  usgrexilem  26257  cffldtocusgr  26264  rgrusgrprc  26389  rusgrprc  26390  rgrprcx  26392  rgrx0ndm  26393  usgr2pthlem  26562  pthdlem2  26567  uspgrn2crct  26603  wwlksnext  26691  wwlksnfi  26704  disjxwwlkn  26711  2wspiundisj  26758  clwwlksndisj  26873  0ewlk  26875  0wlk  26877  0pth  26886  1pthdlem1  26895  1trld  26902  wlk2v2elem2  26916  wlk2v2e  26917  upgr3v3e3cycl  26940  upgr4cycl4dv4e  26945  dfconngr1  26948  0conngr  26952  konigsbergumgr  27012  konigsbergupgrOLD  27013  2wspmdisj  27093  numclwwlk3lem  27130  ex-dif  27168  ex-in  27170  ex-eprel  27178  ex-id  27179  ex-fl  27192  ex-mod  27194  ex-hash  27198  avril1  27207  2bornot2b  27208  0vfval  27349  vsfval  27376  ajmoi  27602  ajfuni  27603  normlem2  27856  norm3adifii  27893  hhip  27922  hlim0  27980  hlimcaui  27981  hlimf  27982  hhssnv  28009  shscli  28064  shsval2i  28134  h1de2i  28300  fh3i  28370  fh4i  28371  cm2mi  28373  qlaxr3i  28383  mayetes3i  28476  ho0f  28498  hoif  28501  hodidi  28534  ho0subi  28542  hosd1i  28569  adjmo  28579  nmopsetn0  28612  nmfnsetn0  28625  funadj  28633  funcnvadj  28640  nmcexi  28773  cnlnadjlem8  28821  nmoptri2i  28846  opsqrlem4  28890  hmopidmchi  28898  pjoci  28927  pjinvari  28938  abrexdomjm  29233  elim2ifim  29252  iundisj2f  29289  rinvf1o  29317  funcnvmptOLD  29351  dfcnv2  29360  snct  29375  fpwrelmap  29392  fzodif2  29435  iundisj2fi  29439  gsumle  29606  xrge0slmod  29671  xrge0pluscn  29810  zlmds  29832  zlmtset  29833  qqhre  29888  esumrnmpt2  29953  esumfsup  29955  esumpcvgval  29963  hasheuni  29970  esumcvg  29971  esumcvgsum  29973  esumsup  29974  esum2d  29978  dmsigagen  30030  ldgenpisyslem3  30051  measvuni  30100  voliune  30115  volfiniune  30116  br2base  30154  dya2iocuni  30168  eulerpartlem1  30252  eulerpartlemt  30256  eulerpartgbij  30257  fib0  30284  coinfliprv  30367  ballotlem2  30373  ballotlemic  30391  ballotlem7  30420  ballotth  30422  plymul02  30445  bnj226  30563  bnj1101  30616  bnj110  30689  bnj149  30706  bnj150  30707  bnj151  30708  bnj517  30716  bnj580  30744  bnj865  30754  bnj900  30760  bnj996  30786  bnj1110  30811  bnj1133  30818  bnj1128  30819  bnj1145  30822  bnj1137  30824  bnj1171  30829  bnj1176  30834  subfacp1lem5  30927  subfacp1lem6  30928  kur14lem9  30957  cvmcov2  31018  cvmliftlem1  31028  cvmliftlem4  31031  cvmliftlem5  31032  msrfo  31204  problem5  31324  brtpid1  31364  brtpid2  31365  brtpid3  31366  logi  31381  faclimlem1  31390  domep  31452  axextndbi  31464  poseq  31504  frrlem10  31545  sltval2  31563  nosepnelem  31618  nosino  31628  brv  31679  txprel  31681  relsset  31690  relbigcup  31699  fvbigcup  31704  fnsingle  31721  fvsingle  31722  snelsingles  31724  funimage  31730  fullfunfnv  31748  imagesset  31755  funtransport  31833  colinrel  31859  funray  31942  funline  31944  0hf  31979  neibastop2lem  32050  filnetlem3  32070  waj-ax  32108  lukshef-ax2  32109  arg-ax  32110  limsucncmpi  32139  dnizeq0  32160  knoppcnlem8  32185  knoppcnlem11  32188  cnndvlem1  32223  bj-babylob  32284  bj-ax12ssb  32330  bj-dvdemo1  32498  bj-disjcsn  32636  bj-snsetex  32651  bj-0eltag  32666  bj-2upln0  32711  bj-2upln1upl  32712  f1omptsnlem  32854  f1omptsn  32855  icoreresf  32871  relowlssretop  32882  relowlpssretop  32883  pigt3  33073  matunitlindf  33078  poimirlem3  33083  poimirlem9  33089  poimirlem16  33096  poimirlem17  33097  poimirlem18  33098  poimirlem19  33099  poimirlem20  33100  poimirlem26  33106  mblfinlem1  33117  mblfinlem2  33118  ismblfin  33121  voliunnfl  33124  cnambfre  33129  cover2  33179  abrexdom  33196  fdc  33212  cncfres  33235  heibor1lem  33279  grposnOLD  33352  bicontr  33550  an12i  33571  tsim1  33608  ac6s6f  33652  ax13fromc9  33710  dedths  33767  renegclALT  33768  hlhilslem  36749  moxfr  36774  mapfzcons1  36799  diophrw  36841  0dioph  36861  vdioph  36862  rabren3dioph  36898  2nn0ind  37029  rpnnen3  37118  kelac2lem  37153  frlmpwfi  37187  ifpbiidcor2  37348  relintabex  37407  eliunov2  37491  xphe  37596  0he  37597  he0  37599  snhesn  37601  idhe  37602  frege54cor1c  37730  clsk1independent  37865  neicvgnvor  37935  amgm2d  38022  amgm3d  38023  amgm4d  38024  lhe4.4ex1a  38049  rusbcALT  38161  ipo0  38174  ifr0  38175  vk15.4j  38255  2sb5nd  38297  dfvd1ir  38310  dfvd2anir  38321  dfvd2ir  38323  dfvd3ir  38330  dfvd3anir  38333  iden2  38360  e0bir  38525  uun2221p1  38562  uun2221p2  38563  2sb5ndVD  38668  2sb5ndALT  38690  iunconnlem2  38693  fnchoice  38710  unisn0  38744  eliincex  38817  icof  38920  mptssid  38960  fsumiunss  39243  resincncf  39423  dvnprodlem3  39500  mbf0  39510  volioc  39525  volico  39537  dmvolss  39539  volioof  39541  stoweidlem13  39567  stoweidlem34  39588  stirlinglem5  39632  stirlinglem13  39640  stirlingr  39644  fourierdlem42  39703  fourierdlem62  39722  fouriersw  39785  etransc  39837  salexct  39889  salexct2  39894  salgencntex  39898  sge0rnn0  39922  gsumge0cl  39925  sge00  39930  sge0resplit  39960  sge0reuz  40001  omeiunle  40068  0ome  40080  icoresmbl  40094  ovn0lem  40116  ovnhoilem1  40152  hspmbl  40180  ovolval5lem3  40205  nsssmfmbf  40324  mbfpsssmf  40328  smfresal  40332  smfmullem4  40338  smfpimbor1lem1  40342  smfpimbor1lem2  40343  aistia  40398  aisfina  40399  aiffnbandciffatnotciffb  40405  axorbciffatcxorb  40406  abnotbtaxb  40416  abnotataxb  40417  pfx2  40741  m3prm  40835  m7prm  40845  0noddALTV  40929  2noddALTV  40933  nnsum3primes4  40995  evengpop3  41005  spr0nelg  41044  oddinmgm  41133  2zrngamgm  41257  2zrngaabl  41262  2zrngmmgm  41264  2zrngnring  41270  fldhmsubc  41402  fldhmsubcALTV  41420  eliunxp2  41430  zlmodzxzldeplem  41605  zlmodzxzldep  41611  ldepslinc  41616  ex-gte  41793  empty-surprise  41861  eximp-surprise2  41864  amgmw2d  41883
  Copyright terms: Public domain W3C validator