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

Theorem mpbir 222
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 219 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  pm5.74ri  263  con4bii  312  imnani  389  mpbir2an  693  imorri  873  orri  880  mpbir3an  1434  xorexmid  1634  tru  1642  had1  1697  nic-mpALT  1752  nic-ax  1753  nic-axALT  1754  nfi  1868  mpgbir  1881  nfxfr  1938  19.35ri  1969  nfxfrOLD  1999  ax5e  2003  ax6ev  2070  ax13  2423  ax13ALT  2473  euequi  2638  moanmo  2696  axi12  2782  axext2  2785  axextmo  2789  eqeltri  2881  nfcxfr  2946  neir  2981  neirr  2987  eqnetri  3048  nelir  3084  mprgbir  3115  vex  3394  issetri  3404  moeq  3574  moeqOLD  3580  rmoeq  3603  cdeqi  3618  eqsstri  3832  3sstr4i  3841  rabnc  4160  tpid1  4494  tpid2  4495  mosneq  4561  pwv  4627  uni0  4659  int0  4683  eqbrtri  4865  tr0  4957  trv  4958  zfrep4  4973  zfnuleuOLD  4980  axnulALT  4981  0ex  4984  inex1  4994  elpwi2  5021  0elpw  5026  axpow2  5037  axpow3  5038  dvdemo1  5043  vpwex  5047  zfpair2  5097  exss  5121  brv  5130  opwo0id  5150  moop2  5155  pwundif  5216  0sn0ep  5228  po0  5247  epse  5294  relxp  5328  relsnopOLD  5430  rel0  5445  relopabi  5447  relopabiALT  5448  eliunxp  5461  opeliunxp2  5462  dmi  5541  xpidtr  5729  xpima  5787  cnvcnv  5797  cnvcnvOLD  5798  dmsn0  5813  cnvsn0  5814  0elon  5990  funmpt  6135  funmpt2  6136  funcnv0  6162  isarep2  6185  fresaunres2  6287  f0  6297  f10  6381  f10d  6382  f1o00  6383  f1oi  6386  f1osn  6388  brprcneu  6396  opabiotafun  6476  fvopab3ig  6495  opabex  6704  mptexgf  6706  eufnfv  6712  isof1oopb  6795  canth  6828  ncanth  6829  mpt2fun  6988  reldmmpt2  6997  ovid  7003  ovidig  7004  ovidi  7005  ovig  7008  ov3  7023  caovmo  7097  relmptopab  7109  porpss  7167  uniex2  7178  snnexOLD  7193  tfinds2  7289  finds  7318  finds2  7320  oprabex  7382  oprabex3  7383  f1stres  7418  f2ndres  7419  relmpt2opab  7489  opeliunxp2f  7567  tpos0  7613  wfrrel  7652  wfrlem14  7660  wfrlem16  7662  issmo  7677  tfrlem6  7710  tfrlem8  7712  tfrlem16  7721  tfr1a  7722  tfr1  7725  tz7.44lem1  7733  seqomlem2  7778  seqomlem3  7779  seqomlem4  7780  fnseqom  7782  0lt1o  7817  0we1  7819  eqer  8010  ecopover  8083  mapsnf1o3  8139  ssdomg  8234  ensn1  8252  snfi  8273  xpcomf1o  8284  map2xp  8365  limensuci  8371  sdom1  8395  unblem4  8450  fidomdm  8478  marypha1lem  8574  hartogslem1  8682  hartogs  8684  card2on  8694  nelaneq  8739  epinid0  8740  ruALT  8743  cnvepnep  8746  inf2  8763  inf3lem6  8773  infeq5i  8776  zfinf2  8782  cantnflt  8812  cnfcom  8840  trcl  8847  tz9.1c  8849  tc2  8861  r1funlim  8872  r1fnon  8873  karden  9001  tskwe  9055  cardprclem  9084  pm54.43  9105  r0weon  9114  iunmapdisj  9125  alephfnon  9167  alephfplem4  9209  alephfp  9210  alephval3  9212  aceq3lem  9222  kmlem2  9254  cda1dif  9279  ackbij1  9341  ackbij2lem2  9343  ackbij2  9346  infpssrlem3  9408  hsmexlem4  9532  hsmexlem5  9533  axdc3lem4  9556  ac2  9564  axac3  9567  ac6  9583  axdclem2  9623  dmct  9627  ondomon  9666  alephsucpw  9673  pwcfsdom  9686  cfpwsdom  9687  smobeth  9689  axpowndlem3  9702  zfcndun  9718  zfcndpow  9719  zfcndinf  9721  zfcndac  9722  wunex2  9841  uniwun  9843  wuncval2  9850  grur1  9923  axgroth5  9927  axgroth2  9928  axgroth6  9931  axgroth3  9934  grothtsk  9938  inaprc  9939  ltsopi  9991  dmaddpi  9993  dmmulpi  9994  1lt2pi  10008  nqerf  10033  addnqf  10051  mulnqf  10052  1lt2nq  10076  m1p1sr  10194  m1m1sr  10195  0lt1sr  10197  axaddf  10247  axmulf  10248  ax1cn  10251  subaddrii  10651  ixi  10937  recgt0ii  11210  nn1suc  11322  neg1lt0  11405  4d2e2  11457  arch  11552  un0mulcl  11589  pnf0xnn0  11632  3halfnz  11718  nummac  11800  uzf  11903  indstr  11971  mnfltpnf  12172  ixxf  12399  ioof  12486  fzf  12549  0nelfz1  12579  fzp1disj  12618  fzp1nel  12643  fzof  12687  om2uzrani  12971  om2uzf1oi  12972  uzrdglem  12976  uzrdgfni  12977  uzrdg0i  12978  ltwenn  12981  hashgf1o  12990  axdc4uzlem  13002  sq0  13174  irec  13183  facmapnn  13288  hashkf  13335  hashfxnn0  13340  hashf  13341  hashfOLD  13342  hash0  13372  prhash2ex  13400  hashsslei  13426  hashxplem  13433  hashbclem  13449  hashf1lem1  13452  wrdexg  13522  s1dm  13599  revs1  13734  0csh0  13759  cshw1  13788  cats1fvn  13823  s2dm  13855  funcnvs1  13877  relexp0g  13981  relexpsucnnr  13984  dfrtrclrec2  14016  rtrclreclem1  14017  rtrclreclem2  14018  rtrclreclem4  14020  dfrtrcl2  14021  climmo  14507  fsumcom2  14724  ackbijnn  14778  incexclem  14786  infcvgaux1i  14807  fprodcom2  14931  fprodn0f  14938  fprodge0  14940  fprodge1  14942  bpolylem  14995  bpoly3  15005  bpoly4  15006  efcvgfsum  15032  cos1bnd  15133  cos2bnd  15134  znnen  15157  qnnen  15158  aleph1re  15190  3dvds  15271  n2dvdsm1  15321  n2dvds3  15323  divalglem5  15336  flodddiv4  15352  bitsf  15364  sadcaddlem  15394  sadadd2lem  15396  sadadd3  15398  sadaddlem  15403  lcmf0  15562  lcmfunsnlem2lem1  15566  lcmfunsnlem2  15568  coprmprod  15589  coprmproddvdslem  15590  2prm  15619  3lcm2e6  15653  phicl2  15686  pockthi  15824  unbenlem  15825  prmrec  15839  vdwlem13  15910  vdwnn  15915  ramcl2  15933  prmgapprmo  15979  mod2xnegi  15988  modsubi  15989  prmo4  16042  prmo5  16043  prmo6  16044  structcnvcnv  16078  setsres  16108  strfv  16114  strlemor1OLD  16176  strleun  16179  0rest  16291  firest  16294  restid  16295  prdsval  16316  prdsbas  16318  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  prdsds  16325  imasaddfnlem  16389  imasvscafn  16398  oppchomfval  16574  oppcbas  16578  2oppchomf  16584  rescbas  16689  rescco  16692  rescabs  16693  0ssc  16697  0subcat  16698  idfucl  16741  wunnat  16816  homarel  16886  dmaf  16899  cdaf  16900  catcfuccl  16959  relxpchom  17022  catcxpccl  17048  oppchofcl  17101  oyoncl  17111  odubas  17334  letsr  17428  mgmidmo  17460  releqg  17839  ga0  17928  oppglem  17977  psgnunilem3  18113  psgnunilem4  18114  pmtrsn  18136  efgval  18327  efger  18328  efgsp1  18347  efgsfo  18349  efgredleme  18353  efgredlem  18357  efgred  18358  cygctb  18490  gsum2d2lem  18569  gsum2d2  18570  gsumcom2  18571  dprd2d2  18641  pgpfaclem1  18678  mgplem  18692  mgpress  18698  opprlem  18826  reldvdsr  18842  00lsp  19184  sralem  19382  srasca  19386  sravsca  19387  psrvscafval  19595  opsrbaslem  19682  psrbag0  19698  00ply1bas  19814  ply1plusgfvi  19816  cnfldfun  19962  cnfldfunALT  19963  xrsmgm  19985  zlmsca  20073  znbaslem  20090  resubdrg  20159  ocvfval  20216  ocv0  20227  cssval  20232  thlbas  20246  thlle  20247  islinds2  20358  matsca  20427  m2detleib  20644  tgdom  20992  tgidm  20994  indistps2ALT  21028  restbas  21172  resttopon  21175  rest0  21183  leordtval2  21226  iocpnfordt  21229  icomnfordt  21230  iooordt  21231  cnpfval  21248  iscnp2  21253  ist1-3  21363  1stcfb  21458  islly2  21497  comppfsc  21545  1stckgen  21567  ptbasfi  21594  xkotf  21598  dfac14  21631  opnfbas  21855  hauspwpwf1  22000  alexsubALTlem4  22063  alexsubALT  22064  ptcmplem5  22069  cnextrel  22076  ust0  22232  tuslem  22280  0met  22380  prdsdsf  22381  prdsxmetlem  22382  prdsmet  22384  setsmsbas  22489  setsmsds  22490  prdsbl  22505  tngds  22661  qtopbaslem  22771  xrtgioo  22818  xrsdsre  22822  zcld  22825  recld2  22826  sszcld  22829  reperflem  22830  retopconn  22841  iccpnfcnv  22952  bndth  22966  ishtpy  22980  nmoleub2lem2  23124  zclmncvs  23156  recmet  23328  resscdrg  23362  ishl2  23374  recms  23376  volf  23506  iundisj2  23526  volsup  23533  icombl  23541  ioombl  23542  ismbf3d  23631  0plef  23649  0pledm  23650  itg1ge0  23663  mbfi1fseqlem5  23696  itg2addlem  23735  iblcnlem1  23764  reldv  23844  limciun  23868  dvexp  23926  dveflem  23952  lhop1lem  23986  lhop  23989  elply2  24162  elplyd  24168  ply1term  24170  ply0  24174  plymullem  24182  qaa  24288  pserulm  24386  pserdvlem2  24392  efcn  24407  sincosq1lem  24460  tangtx  24468  sincos4thpi  24476  sincos6thpi  24478  pige3  24480  efif1olem4  24502  logf1o  24521  relogf1o  24523  log1  24542  loge  24543  relogiso  24554  dvrelog  24593  relogcn  24594  logcn  24603  cxpcn3  24699  resqrtcn  24700  leibpi  24879  log2ublem1  24883  birthday  24891  emcllem5  24936  harmonicbnd  24940  harmonicbnd2  24941  emgt0  24943  harmonicbnd3  24944  lgamgulm2  24972  lgamcvglem  24976  gamf  24979  ppiltx  25113  ppiublem1  25137  ppiub  25139  bclbnd  25215  bpos1lem  25217  bposlem8  25226  lgsquadlem2  25316  2sqlem9  25362  2sqlem10  25363  chebbnd1  25371  selberg2lem  25449  pntrsumo1  25464  selbergsb  25474  pntpbnd  25487  istrkg2ld  25569  tgcgr4  25636  ttgval  25965  ttglem  25966  cchhllem  25977  ax5seglem7  26025  axlowdimlem4  26035  axlowdimlem6  26037  axlowdimlem7  26038  axlowdimlem10  26041  axlowdimlem13  26044  axlowdimlem16  26047  uhgr0e  26176  uhgr0  26178  upgrbi  26198  umgrbi  26206  usgr0  26347  lfuhgr1v0e  26358  usgrexmpllem  26364  usgrexmpl  26367  griedg0prc  26368  cplgr0  26545  usgrexilem  26560  cffldtocusgr  26567  rgrusgrprc  26709  rusgrprc  26710  rgrprcx  26712  rgrx0ndm  26713  usgr2pthlem  26883  pthdlem2  26888  uspgrn2crct  26925  wwlksnext  27026  wwlksnfi  27039  disjxwwlkn  27047  clwwlknondisj  27276  clwwlknondisjOLD  27281  0ewlk  27283  0wlk  27285  0pth  27294  1pthdlem1  27304  1trld  27311  wlk2v2elem2  27325  wlk2v2e  27326  upgr3v3e3cycl  27349  upgr4cycl4dv4e  27354  dfconngr1  27357  0conngr  27361  konigsbergumgr  27420  2wspmdisj  27508  2clwwlk2clwwlk  27523  numclwwlk3lemOLD  27565  numclwwlk3lem2lem  27567  numclwwlk3lem2  27568  ex-dif  27607  ex-in  27609  ex-eprel  27617  ex-id  27618  ex-fl  27631  ex-mod  27633  ex-hash  27637  avril1  27646  2bornot2b  27647  0vfval  27785  vsfval  27812  ajmoi  28038  ajfuni  28039  normlem2  28292  norm3adifii  28329  hhip  28358  hlim0  28416  hlimcaui  28417  hlimf  28418  hhssnv  28445  shscli  28500  shsval2i  28570  h1de2i  28736  fh3i  28806  fh4i  28807  cm2mi  28809  qlaxr3i  28819  mayetes3i  28912  ho0f  28934  hoif  28937  hodidi  28970  ho0subi  28978  hosd1i  29005  adjmo  29015  nmopsetn0  29048  nmfnsetn0  29061  funadj  29069  funcnvadj  29076  nmcexi  29209  cnlnadjlem8  29257  nmoptri2i  29282  opsqrlem4  29326  hmopidmchi  29334  pjoci  29363  pjinvari  29374  abrexdomjm  29666  elim2ifim  29685  iundisj2f  29724  rinvf1o  29755  funcnvmptOLD  29790  dfcnv2  29799  snct  29814  fpwrelmap  29831  fzodif2  29875  iundisj2fi  29879  dp2lt10  29913  dp2ltc  29916  dplti  29934  dpgti  29935  dpexpp1  29937  gsumle  30100  xrge0slmod  30165  xrge0pluscn  30307  zlmds  30329  zlmtset  30330  qqhre  30385  esumrnmpt2  30451  esumfsup  30453  esumpcvgval  30461  hasheuni  30468  esumcvg  30469  esumcvgsum  30471  esumsup  30472  esum2d  30476  dmsigagen  30528  ldgenpisyslem3  30549  measvuni  30598  voliune  30613  volfiniune  30614  br2base  30652  dya2iocuni  30666  eulerpartlem1  30750  eulerpartlemt  30754  eulerpartgbij  30755  fib0  30782  coinfliprv  30865  ballotlem2  30871  ballotlemic  30889  ballotlem7  30918  ballotth  30920  plymul02  30944  rpsqrtcn  30992  chtvalz  31028  circlemethnat  31040  circlevma  31041  circlemethhgt  31042  hgt750lem  31050  bnj226  31121  bnj1101  31173  bnj110  31246  bnj149  31263  bnj150  31264  bnj151  31265  bnj517  31273  bnj580  31301  bnj865  31311  bnj900  31317  bnj996  31343  bnj1110  31368  bnj1133  31375  bnj1128  31376  bnj1145  31379  bnj1137  31381  bnj1171  31386  bnj1176  31391  subfacp1lem5  31484  subfacp1lem6  31485  kur14lem9  31514  cvmcov2  31575  cvmliftlem1  31585  cvmliftlem4  31588  cvmliftlem5  31589  msrfo  31761  problem5  31880  brtpid1  31919  brtpid2  31920  brtpid3  31921  logi  31937  faclimlem1  31946  domep  32013  axextndbi  32025  poseq  32069  frrlem6  32105  frrlem10  32107  sltval2  32125  noxp1o  32132  nosepnelem  32146  txprel  32302  relsset  32311  relbigcup  32320  fvbigcup  32325  fnsingle  32342  fvsingle  32343  snelsingles  32345  funimage  32351  fullfunfnv  32369  imagesset  32376  funtransport  32454  colinrel  32480  funray  32563  funline  32565  0hf  32600  neibastop2lem  32671  filnetlem3  32691  waj-ax  32725  lukshef-ax2  32726  arg-ax  32727  limsucncmpi  32756  dnizeq0  32777  knoppcnlem8  32802  knoppcnlem11  32805  cnndvlem1  32840  bj-babylob  32899  bj-ax12ssb  32946  bj-dvdemo1  33111  bj-disjcsn  33242  bj-snsetex  33256  bj-0eltag  33271  bj-2upln0  33316  bj-2upln1upl  33317  f1omptsnlem  33495  f1omptsn  33496  icoreresf  33511  relowlssretop  33522  relowlpssretop  33523  cnfinltrel  33552  pigt3  33710  matunitlindf  33715  poimirlem3  33720  poimirlem9  33726  poimirlem16  33733  poimirlem17  33734  poimirlem18  33735  poimirlem19  33736  poimirlem20  33737  poimirlem26  33743  mblfinlem1  33754  mblfinlem2  33755  ismblfin  33758  voliunnfl  33761  cnambfre  33765  cover2  33815  abrexdom  33832  fdc  33847  cncfres  33870  heibor1lem  33914  grposnOLD  33987  bicontr  34185  an12i  34206  tsim1  34242  ac6s6f  34286  vvdifopab  34337  opabf  34438  xrnrel  34443  relcoels  34487  cnvcosseq  34500  refrelcoss3  34521  refrelcoss2  34522  symrelcoss2  34524  refrelcoss  34580  symrelcoss  34614  ax13fromc9  34680  dedths  34736  renegclALT  34737  hlhilslem  37713  moxfr  37751  mapfzcons1  37776  diophrw  37818  0dioph  37838  vdioph  37839  rabren3dioph  37875  2nn0ind  38005  rpnnen3  38094  kelac2lem  38129  frlmpwfi  38163  ifpbiidcor2  38322  relintabex  38381  eliunov2  38465  xphe  38569  0he  38570  he0  38572  snhesn  38574  idhe  38575  frege54cor1c  38703  clsk1independent  38838  neicvgnvor  38908  amgm2d  38995  amgm3d  38996  amgm4d  38997  lhe4.4ex1a  39022  rusbcALT  39133  ipo0  39145  ifr0  39146  vk15.4j  39226  2sb5nd  39268  dfvd1ir  39281  dfvd2anir  39292  dfvd2ir  39294  dfvd3ir  39301  dfvd3anir  39304  iden2  39331  e0bir  39495  uun2221p1  39532  uun2221p2  39533  2sb5ndVD  39634  2sb5ndALT  39656  iunconnlem2  39659  fnchoice  39676  unisn0  39709  eliincex  39779  icof  39892  mptssid  39928  supminfxr  40167  fsumiunss  40281  climlimsupcex  40475  liminfltlimsupex  40487  liminflelimsupcex  40503  xlimrel  40520  resincncf  40562  dvnprodlem3  40637  volioc  40661  volico  40673  dmvolss  40675  volioof  40677  stoweidlem13  40703  stoweidlem34  40724  stirlinglem5  40768  stirlinglem13  40776  stirlingr  40780  fourierdlem42  40839  fourierdlem62  40858  fouriersw  40921  etransc  40973  salexct  41025  salexct2  41030  salgencntex  41034  sge0rnn0  41058  gsumge0cl  41061  sge00  41066  sge0resplit  41096  sge0reuz  41137  omeiunle  41207  0ome  41219  icoresmbl  41233  ovn0lem  41255  ovnhoilem1  41291  hspmbl  41319  ovolval5lem3  41344  nsssmfmbf  41463  mbfpsssmf  41467  smfresal  41471  smfmullem4  41477  smfpimbor1lem1  41481  smfpimbor1lem2  41482  aistia  41540  aisfina  41541  aiffnbandciffatnotciffb  41547  axorbciffatcxorb  41548  abnotbtaxb  41558  abnotataxb  41559  eusnsn  41644  aiotaval  41671  aiota0ndef  41673  pfx2  41981  m3prm  42075  m7prm  42085  0noddALTV  42169  2noddALTV  42173  sbgoldbo  42244  nnsum3primes4  42245  evengpop3  42255  spr0nelg  42288  oddinmgm  42377  2zrngamgm  42501  2zrngaabl  42506  2zrngmmgm  42508  2zrngnring  42514  fldhmsubc  42646  fldhmsubcALTV  42664  eliunxp2  42674  zlmodzxzldeplem  42849  zlmodzxzldep  42855  ldepslinc  42860  ex-gte  43035  empty-surprise  43093  eximp-surprise2  43096  amgmw2d  43115
  Copyright terms: Public domain W3C validator