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

Theorem mpbir 220
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 217 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  pm5.74ri  260  con4bii  310  orri  390  imorri  429  imnani  438  mpbir2an  957  mpbir3an  1237  xorexmid  1472  tru  1479  had1  1533  nic-mpALT  1588  nic-ax  1589  nic-axALT  1590  nfi  1705  mpgbir  1717  nfxfr  1771  19.35ri  1796  nfxfrOLD  1825  ax5e  1829  ax6ev  1877  exanOLDOLD  2155  ax13  2237  ax13OLD  2293  euequ1  2464  moanmo  2520  axi12  2588  axext2  2591  eqeltri  2684  nfcxfr  2749  neir  2785  neirr  2791  eqnetri  2852  nelir  2886  mprgbir  2911  vex  3176  issetri  3183  moeq  3349  rmoeq  3372  cdeqi  3387  eqsstri  3598  3sstr4i  3607  elini  3759  rabnc  3916  tpid1  4246  tpid2  4247  pwv  4371  uni0  4401  int0  4425  eqbrtri  4604  tr0  4692  trv  4693  zfrep4  4707  zfnuleu  4714  axnulALT  4715  0ex  4718  inex1  4727  0elpw  4760  axpow2  4771  axpow3  4772  pwex  4774  dvdemo1  4829  zfpair2  4834  exss  4858  moop2  4891  pwundif  4945  po0  4974  epse  5021  relsnop  5147  relxp  5150  rel0  5166  relopabi  5167  relopabiALT  5168  eliunxp  5181  opeliunxp2  5182  dmi  5261  xpidtr  5437  xpima  5495  cnvcnv  5505  dmsn0  5520  cnvsn0  5521  0elon  5695  funmpt  5840  funmpt2  5841  funcnv0  5869  isarep2  5892  fresaunres2  5989  f0  5999  f10  6081  f10d  6082  f1o00  6083  f1oi  6086  f1osn  6088  brprcneu  6096  opabiotafun  6169  fvopab3ig  6188  opabex  6388  eufnfv  6395  isof1oopb  6475  canth  6508  ncanth  6509  mpt2fun  6660  reldmmpt2  6669  ovid  6675  ovidig  6676  ovidi  6677  ovig  6680  ov3  6695  caovmo  6769  relmptopab  6781  porpss  6839  uniex2  6850  snnex  6862  tfinds2  6955  finds  6984  finds2  6986  oprabex  7047  oprabex3  7048  f1stres  7081  f2ndres  7082  relmpt2opab  7146  opeliunxp2f  7223  tpos0  7269  wfrrel  7307  wfrlem14  7315  wfrlem16  7317  issmo  7332  tfrlem6  7365  tfrlem8  7367  tfrlem16  7376  tfr1a  7377  tfr1  7380  tz7.44lem1  7388  seqomlem2  7433  seqomlem3  7434  seqomlem4  7435  fnseqom  7437  0lt1o  7471  0we1  7473  eqer  7664  eqerOLD  7665  ecopover  7738  ecopoverOLD  7739  mapsnf1o3  7792  ssdomg  7887  ensn1  7906  snfi  7923  xpcomf1o  7934  map2xp  8015  limensuci  8021  sdom1  8045  unblem4  8100  fidomdm  8128  marypha1lem  8222  hartogslem1  8330  hartogs  8332  card2on  8342  ruALT  8391  inf2  8403  inf3lem6  8413  infeq5i  8416  zfinf2  8422  cantnflt  8452  cnfcom  8480  trcl  8487  tz9.1c  8489  tc2  8501  r1funlim  8512  r1fnon  8513  karden  8641  tskwe  8659  cardprclem  8688  pm54.43  8709  r0weon  8718  iunmapdisj  8729  alephfnon  8771  alephfplem4  8813  alephfp  8814  alephval3  8816  aceq3lem  8826  kmlem2  8856  cda1dif  8881  ackbij1  8943  ackbij2lem2  8945  ackbij2  8948  infpssrlem3  9010  hsmexlem4  9134  hsmexlem5  9135  axdc3lem4  9158  ac2  9166  axac3  9169  ac6  9185  axdclem2  9225  ondomon  9264  alephsucpw  9271  pwcfsdom  9284  cfpwsdom  9285  smobeth  9287  axpowndlem3  9300  zfcndun  9316  zfcndpow  9317  zfcndinf  9319  zfcndac  9320  wunex2  9439  uniwun  9441  wuncval2  9448  grur1  9521  axgroth5  9525  axgroth2  9526  axgroth6  9529  axgroth3  9532  grothtsk  9536  inaprc  9537  ltsopi  9589  dmaddpi  9591  dmmulpi  9592  1lt2pi  9606  nqerf  9631  addnqf  9649  mulnqf  9650  1lt2nq  9674  m1p1sr  9792  m1m1sr  9793  0lt1sr  9795  axaddf  9845  axmulf  9846  ax1cn  9849  subaddrii  10249  ixi  10535  recgt0ii  10808  nn1suc  10918  neg1lt0  11004  4d2e2  11061  arch  11166  un0mulcl  11204  pnf0xnn0  11247  3halfnz  11332  nummac  11434  uzf  11566  indstr  11632  mnfltpnf  11836  ixxf  12056  ioof  12142  fzf  12201  0nelfz1  12231  fzp1disj  12269  fzp1nel  12293  fzof  12336  om2uzrani  12613  om2uzf1oi  12614  uzrdglem  12618  uzrdgfni  12619  uzrdg0i  12620  ltwenn  12623  hashgf1o  12632  axdc4uzlem  12644  sq0  12817  irec  12826  facmapnn  12934  hashkf  12981  hashfxnn0  12986  hashf  12987  hashfOLD  12988  hash0  13019  prhash2ex  13048  hashsslei  13073  hashxplem  13080  hashbclem  13093  hashf1lem1  13096  fundmge2nop0  13129  wrdexg  13170  s1dm  13241  revs1  13365  0csh0  13390  cshw1  13419  cats1fvn  13454  s2dm  13485  funcnvs1  13507  relexp0g  13610  relexpsucnnr  13613  dfrtrclrec2  13645  rtrclreclem1  13646  rtrclreclem2  13647  rtrclreclem4  13649  dfrtrcl2  13650  climmo  14136  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  incexclem  14407  infcvgaux1i  14428  fprodcom2  14553  fprodcom2OLD  14554  fprodn0f  14561  fprodge0  14563  fprodge1  14565  bpolylem  14618  bpoly3  14628  bpoly4  14629  efcvgfsum  14655  cos1bnd  14756  cos2bnd  14757  znnen  14780  qnnen  14781  aleph1re  14813  3dvds  14890  3dvdsOLD  14891  n2dvdsm1  14943  n2dvds3  14945  divalglem5  14958  flodddiv4  14975  bitsf  14987  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  lcmf0  15185  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  coprmprod  15213  coprmproddvdslem  15214  2prm  15243  3lcm2e6  15278  phicl2  15311  pockthi  15449  unbenlem  15450  prmrec  15464  vdwlem13  15535  vdwnn  15540  ramcl2  15558  prmgapprmo  15604  mod2xnegi  15613  modsubi  15614  prmo4  15673  prmo5  15674  prmo6  15675  structcnvcnv  15706  structfun  15707  setsres  15729  strfv  15735  strlemor1  15796  strleun  15799  0rest  15913  firest  15916  restid  15917  prdsval  15938  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdsds  15947  imasaddfnlem  16011  imasvscafn  16020  oppchomfval  16197  oppcbas  16201  2oppchomf  16207  rescbas  16312  rescco  16315  rescabs  16316  0ssc  16320  0subcat  16321  idfucl  16364  wunnat  16439  homarel  16509  dmaf  16522  cdaf  16523  catcfuccl  16582  relxpchom  16644  catcxpccl  16670  oppchofcl  16723  oyoncl  16733  odubas  16956  letsr  17050  mgmidmo  17082  releqg  17464  ga0  17554  oppglem  17603  psgnunilem3  17739  psgnunilem4  17740  pmtrsn  17762  efgval  17953  efger  17954  efgsp1  17973  efgsfo  17975  efgredleme  17979  efgredlem  17983  efgred  17984  cygctb  18116  gsum2d2lem  18195  gsum2d2  18196  gsumcom2  18197  dprd2d2  18266  pgpfaclem1  18303  mgplem  18317  mgpress  18323  opprlem  18451  reldvdsr  18467  00lsp  18802  sralem  18998  srasca  19002  sravsca  19003  psrvscafval  19211  opsrbaslem  19298  opsrbaslemOLD  19299  psrbag0  19315  00ply1bas  19431  ply1plusgfvi  19433  xrsmgm  19600  zlmsca  19688  znbaslem  19705  znbaslemOLD  19706  resubdrg  19773  ocvfval  19829  ocv0  19840  cssval  19845  thlbas  19859  thlle  19860  islinds2  19971  matsca  20040  m2detleib  20256  tgdom  20593  tgidm  20595  indistps2ALT  20628  restbas  20772  resttopon  20775  rest0  20783  leordtval2  20826  iocpnfordt  20829  icomnfordt  20830  iooordt  20831  cnpfval  20848  iscnp2  20853  ist1-3  20963  1stcfb  21058  islly2  21097  comppfsc  21145  1stckgen  21167  ptbasfi  21194  xkotf  21198  dfac14  21231  opnfbas  21456  hauspwpwf1  21601  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem5  21670  cnextrel  21677  ust0  21833  tuslem  21881  0met  21981  prdsdsf  21982  prdsxmetlem  21983  prdsmet  21985  setsmsbas  22090  setsmsds  22091  prdsbl  22106  tngds  22262  qtopbaslem  22372  xrtgioo  22417  xrsdsre  22421  zcld  22424  recld2  22425  sszcld  22428  reperflem  22429  retopcon  22440  iccpnfcnv  22551  bndth  22565  ishtpy  22579  nmoleub2lem2  22724  zclmncvs  22756  recmet  22928  resscdrg  22962  ishl2  22974  recms  22976  volf  23104  iundisj2  23124  volsup  23131  icombl  23139  ioombl  23140  ismbf3d  23227  0plef  23245  0pledm  23246  itg1ge0  23259  mbfi1fseqlem5  23292  itg2addlem  23331  iblcnlem1  23360  reldv  23440  limciun  23464  dvexp  23522  dveflem  23546  lhop1lem  23580  lhop  23583  elply2  23756  elplyd  23762  ply1term  23764  ply0  23768  plymullem  23776  qaa  23882  pserulm  23980  pserdvlem2  23986  efcn  24001  sincosq1lem  24053  tangtx  24061  sincos4thpi  24069  sincos6thpi  24071  pige3  24073  efif1olem4  24095  logf1o  24115  relogf1o  24117  log1  24136  loge  24137  relogiso  24148  dvrelog  24183  relogcn  24184  logcn  24193  cxpcn3  24289  resqrtcn  24290  leibpi  24469  log2ublem1  24473  birthday  24481  emcllem5  24526  harmonicbnd  24530  harmonicbnd2  24531  emgt0  24533  harmonicbnd3  24534  lgamgulm2  24562  lgamcvglem  24566  gamf  24569  ppiltx  24703  ppiublem1  24727  ppiub  24729  bclbnd  24805  bpos1lem  24807  bposlem8  24816  lgsquadlem2  24906  2sqlem9  24952  2sqlem10  24953  chebbnd1  24961  selberg2lem  25039  pntrsumo1  25054  selbergsb  25064  pntpbnd  25077  istrkg2ld  25159  tgcgr4  25226  ttgval  25555  ttglem  25556  cchhllem  25567  ax5seglem7  25615  axlowdimlem4  25625  axlowdimlem6  25627  axlowdimlem7  25628  axlowdimlem10  25631  axlowdimlem13  25634  axlowdimlem16  25637  uhgr0e  25737  uhgr0  25739  upgrbi  25760  umgrbi  25767  uhgra0  25838  umgra0  25854  usgra1v  25919  cusgraexilem2  25996  cusgrasizeindslem1  26002  0wlk  26075  0trl  26076  wlkntrllem2  26090  wlkntrl  26092  0pth  26100  1pthonlem1  26119  usgrcyclnl2  26169  4cycl4dv  26195  wwlknext  26252  wwlknfi  26266  disjxwwlkn  26273  vdgrf  26425  umgrabi  26510  vdegp1ai  26511  vdegp1bi  26512  konigsberg  26514  frgra0  26521  numclwwlkdisj  26607  numclwwlk3lem  26635  ex-dif  26672  ex-in  26674  ex-eprel  26682  ex-id  26683  ex-fl  26696  ex-mod  26698  ex-hash  26702  avril1  26711  2bornot2b  26712  0vfval  26845  vsfval  26872  ajmoi  27098  ajfuni  27099  normlem2  27352  norm3adifii  27389  hhip  27418  hlim0  27476  hlimcaui  27477  hlimf  27478  hhssnv  27505  shscli  27560  shsval2i  27630  h1de2i  27796  fh3i  27866  fh4i  27867  cm2mi  27869  qlaxr3i  27879  mayetes3i  27972  ho0f  27994  hoif  27997  hodidi  28030  ho0subi  28038  hosd1i  28065  adjmo  28075  nmopsetn0  28108  nmfnsetn0  28121  funadj  28129  funcnvadj  28136  nmcexi  28269  cnlnadjlem8  28317  nmoptri2i  28342  opsqrlem4  28386  hmopidmchi  28394  pjoci  28423  pjinvari  28434  abrexdomjm  28729  elim2ifim  28748  iundisj2f  28785  mptexgf  28809  rinvf1o  28814  funcnvmptOLD  28850  dfcnv2  28859  snct  28874  dmct  28877  fpwrelmap  28896  iundisj2fi  28943  gsumle  29110  xrge0slmod  29175  xrge0pluscn  29314  zlmds  29336  zlmtset  29337  qqhre  29392  esumrnmpt2  29457  esumfsup  29459  esumpcvgval  29467  hasheuni  29474  esumcvg  29475  esumcvgsum  29477  esumsup  29478  esum2d  29482  dmsigagen  29534  ldgenpisyslem3  29555  measvuni  29604  voliune  29619  volfiniune  29620  br2base  29658  dya2iocuni  29672  eulerpartlem1  29756  eulerpartlemt  29760  eulerpartgbij  29761  fib0  29788  coinfliprv  29871  ballotlem2  29877  ballotlemic  29895  ballotlem7  29924  ballotth  29926  plymul02  29949  bnj226  30056  bnj1101  30109  bnj110  30182  bnj149  30199  bnj150  30200  bnj151  30201  bnj517  30209  bnj580  30237  bnj865  30247  bnj900  30253  bnj996  30279  bnj1110  30304  bnj1133  30311  bnj1128  30312  bnj1145  30315  bnj1137  30317  bnj1171  30322  bnj1176  30327  subfacp1lem5  30420  subfacp1lem6  30421  kur14lem9  30450  cvmcov2  30511  cvmliftlem1  30521  cvmliftlem4  30524  cvmliftlem5  30525  msrfo  30697  problem5  30817  brtpid1  30857  brtpid2  30858  brtpid3  30859  logi  30873  faclimlem1  30882  domep  30942  axextndbi  30954  poseq  30994  frrlem10  31035  sltval2  31053  brv  31154  txprel  31156  relsset  31165  relbigcup  31174  fvbigcup  31179  fnsingle  31196  fvsingle  31197  snelsingles  31199  funimage  31205  fullfunfnv  31223  imagesset  31230  funtransport  31308  colinrel  31334  funray  31417  funline  31419  0hf  31454  neibastop2lem  31525  filnetlem3  31545  waj-ax  31583  lukshef-ax2  31584  arg-ax  31585  limsucncmpi  31614  dnizeq0  31635  knoppcnlem8  31660  knoppcnlem11  31663  cnndvlem1  31698  bj-babylob  31762  bj-nalnalimiOLD  31799  bj-nfv  31806  bj-ax12ssb  31824  bj-dvdemo1  31990  bj-disjcsn  32129  bj-snsetex  32144  bj-0eltag  32159  bj-2upln0  32204  bj-2upln1upl  32205  f1omptsnlem  32359  f1omptsn  32360  icoreresf  32376  relowlssretop  32387  relowlpssretop  32388  pigt3  32572  matunitlindf  32577  poimirlem3  32582  poimirlem9  32588  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem26  32605  mblfinlem1  32616  mblfinlem2  32617  ismblfin  32620  voliunnfl  32623  cnambfre  32628  cover2  32678  abrexdom  32695  fdc  32711  cncfres  32734  heibor1lem  32778  grposnOLD  32851  bicontr  33049  an12i  33070  tsim1  33107  ac6s6f  33151  ax13fromc9  33209  elimhyps  33265  dedths  33266  renegclALT  33267  hlhilslem  36248  moxfr  36273  mapfzcons1  36298  diophrw  36340  0dioph  36360  vdioph  36361  rabren3dioph  36397  2nn0ind  36528  rpnnen3  36617  kelac2lem  36652  frlmpwfi  36686  ifpbiidcor2  36847  relintabex  36906  eliunov2  36990  xphe  37095  0he  37096  he0  37098  snhesn  37100  idhe  37101  frege54cor1c  37229  clsk1independent  37364  neicvgnvor  37434  amgm2d  37523  amgm3d  37524  amgm4d  37525  lhe4.4ex1a  37550  rusbcALT  37662  ipo0  37674  ifr0  37675  vk15.4j  37755  2sb5nd  37797  dfvd1ir  37810  dfvd2anir  37821  dfvd2ir  37823  dfvd3ir  37830  dfvd3anir  37833  iden2  37860  e0bir  38025  uun2221p1  38062  uun2221p2  38063  2sb5ndVD  38168  2sb5ndALT  38190  iunconlem2  38193  fnchoice  38211  unisn0  38247  elpwi2  38291  eliincex  38324  ssrab2f  38331  icof  38406  fsumiunss  38642  resincncf  38760  dvnprodlem3  38838  mbf0  38849  volioc  38864  volico  38876  dmvolss  38878  volioof  38880  stoweidlem13  38906  stoweidlem34  38927  stirlinglem5  38971  stirlinglem13  38979  stirlingr  38983  fourierdlem42  39042  fourierdlem62  39061  fouriersw  39124  etransc  39176  salexct  39228  salexct2  39233  salgencntex  39237  sge0rnn0  39261  gsumge0cl  39264  sge00  39269  sge0resplit  39299  sge0reuz  39340  omeiunle  39407  0ome  39419  icoresmbl  39433  ovn0lem  39455  ovnhoilem1  39491  hspmbl  39519  ovolval5lem3  39544  nsssmfmbf  39665  mbfpsssmf  39669  smfresal  39673  smfmullem4  39679  smfpimbor1lem1  39683  smfpimbor1lem2  39684  aistia  39713  aisfina  39714  aiffnbandciffatnotciffb  39720  axorbciffatcxorb  39721  abnotbtaxb  39731  abnotataxb  39732  m3prm  40044  m7prm  40054  0noddALTV  40138  2noddALTV  40142  nnsum3primes4  40204  evengpop3  40214  pfx2  40275  usgr0  40469  lfuhgr1v0e  40480  usgrexmpllem  40484  usgrexmpl  40487  griedg0prc  40488  cplgr0  40647  usgrexi  40661  rgrusgrprc  40789  rusgrprc  40790  rgrprcx  40792  rgrx0ndm  40793  usgr2pthlem  40969  pthdlem2  40974  uspgrn2crct  41011  wwlksnext  41099  wwlksnfi  41112  av-disjxwwlkn  41119  2wspiundisj  41166  clwwlksndisj  41280  0ewlk  41282  01wlk  41284  0pth-av  41293  1pthdlem1  41302  1trld  41309  1wlk2v2elem2  41323  1wlk2v2e  41324  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  dfconngr1  41355  0conngr  41359  konigsbergumgr  41420  konigsbergupgrOLD  41421  2wspmdisj  41501  av-numclwwlk3lem  41538  oddinmgm  41605  2zrngamgm  41729  2zrngaabl  41734  2zrngmmgm  41736  2zrngnring  41742  fldhmsubc  41876  fldhmsubcALTV  41895  eliunxp2  41905  zlmodzxzldeplem  42081  zlmodzxzldep  42087  ldepslinc  42092  ex-gte  42269  empty-surprise  42337  eximp-surprise2  42340  amgmw2d  42359
  Copyright terms: Public domain W3C validator