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

Theorem mpbir 232
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 229 . 2 (𝜓𝜑)
41, 3ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  pm5.74ri  273  con4bii  322  imnani  401  mpbir2an  707  imorri  849  orri  856  mpbir3an  1333  xorexmid  1511  tru  1532  had1  1595  nic-mpALT  1664  nic-ax  1665  nic-axALT  1666  nfi  1780  mpgbir  1791  nfxfr  1844  19.35ri  1871  ax5e  1904  ax6ev  1963  sbt  2062  equsb1v  2103  ax13  2384  ax13ALT  2439  moanmo  2700  axi12  2786  axi12OLD  2787  axbnd  2788  axexte  2791  axextmo  2794  nulmo  2795  vexw  2802  eqeltri  2906  nfcxfr  2972  neir  3016  neirr  3022  eqnetri  3083  nelir  3123  mprgbir  3150  cbvrexdva2  3455  vexOLD  3496  issetri  3508  moeq  3695  rmoeq  3726  cdeqi  3753  eqsstri  3998  3sstr4i  4007  rmo0  4316  rabnc  4338  reuprg  4631  tpid1  4696  tpid2  4698  mosneq  4765  pwv  4827  uni0  4857  int0  4881  eqbrtri  5078  tr0  5174  trv  5175  zfrep4  5191  axnulALT  5199  0ex  5202  inex1  5212  elpwi2  5240  0elpw  5247  axpow2  5259  axpow3  5260  dvdemo1  5265  vpwex  5269  zfpair2  5321  exss  5346  brv  5355  opwo0id  5378  moop2  5383  pwundifOLD  5450  0sn0ep  5463  po0  5483  epse  5531  relxp  5566  rel0  5665  relopabiv  5686  relopabi  5687  relopabiALT  5688  eliunxp  5701  opeliunxp2  5702  dmi  5784  dmep  5786  domepOLD  5787  xpidtr  5975  xpima  6032  dmsn0  6059  cnvsn0  6060  0elon  6237  funmpt  6386  funmpt2  6387  funcnv0  6413  isarep2  6436  fresaunres2  6543  f0  6553  f10d  6641  f1o00  6642  f1oi  6645  f1osn  6647  brprcneu  6655  opabiotafun  6737  fvopab3ig  6757  opabex  6974  mptexgf  6976  eufnfv  6982  isof1oopb  7067  ncanth  7101  mpofun  7265  reldmmpo  7274  ovid  7280  ovidig  7281  ovidi  7282  ovig  7285  ov3  7300  caovmo  7374  relmptopab  7384  porpss  7442  uniex2  7453  tfinds2  7567  finds  7597  finds2  7599  oprabex  7666  oprabex3  7667  f1stres  7702  f2ndres  7703  relmpoopab  7778  fsplitfpar  7803  opeliunxp2f  7865  tpos0  7911  wfrrel  7949  wfrlem14  7957  wfrlem16  7959  issmo  7974  tfrlem6  8007  tfrlem8  8009  tfrlem16  8018  tfr1a  8019  tfr1  8022  tz7.44lem1  8030  seqomlem2  8076  seqomlem3  8077  seqomlem4  8078  fnseqom  8080  0lt1o  8118  0we1  8120  eqer  8313  ecopover  8390  mapsnf1o3  8447  ssdomg  8543  ensn1  8561  snfi  8582  xpcomf1o  8594  map2xp  8675  limensuci  8681  sdom1  8706  unblem4  8761  fidomdm  8789  marypha1lem  8885  hartogslem1  8994  hartogs  8996  card2on  9006  nelaneq  9051  epinid0  9052  ruALT  9055  elnanel  9058  cnvepnep  9059  inf2  9074  inf3lem6  9084  infeq5i  9087  zfinf2  9093  cantnflt  9123  cnfcom  9151  trcl  9158  tz9.1c  9160  tc2  9172  r1funlim  9183  r1fnon  9184  karden  9312  tskwe  9367  cardprclem  9396  pm54.43  9417  r0weon  9426  iunmapdisj  9437  alephfnon  9479  alephfplem4  9521  alephfp  9522  alephval3  9524  kmlem2  9565  dju1dif  9586  ackbij1  9648  ackbij2lem2  9650  ackbij2  9653  infpssrlem3  9715  hsmexlem4  9839  hsmexlem5  9840  ac2  9871  axac3  9874  ac6  9890  axdclem2  9930  dmct  9934  ondomon  9973  alephsucpw  9980  pwcfsdom  9993  cfpwsdom  9994  smobeth  9996  axpowndlem3  10009  zfcndun  10025  zfcndpow  10026  zfcndinf  10028  zfcndac  10029  wunex2  10148  uniwun  10150  wuncval2  10157  grur1  10230  axgroth5  10234  axgroth2  10235  axgroth6  10238  axgroth3  10241  grothtsk  10245  inaprc  10246  ltsopi  10298  dmaddpi  10300  dmmulpi  10301  1lt2pi  10315  nqerf  10340  addnqf  10358  mulnqf  10359  1lt2nq  10383  m1p1sr  10502  m1m1sr  10503  0lt1sr  10505  axaddf  10555  axmulf  10556  ax1cn  10559  subaddrii  10963  ixi  11257  recgt0ii  11534  nn1suc  11647  neg1lt0  11742  4d2e2  11795  arch  11882  un0mulcl  11919  pnf0xnn0  11962  3halfnz  12049  nummac  12131  indstr  12304  mnfltpnf  12509  ioof  12823  0nelfz1  12914  fzp1disj  12954  fzp1nel  12979  fzof  13023  om2uzrani  13308  om2uzf1oi  13309  uzrdglem  13313  uzrdgfni  13314  uzrdg0i  13315  ltwenn  13318  hashgf1o  13327  axdc4uzlem  13339  sq0  13543  irec  13552  facmapnn  13633  hashkf  13680  hashfxnn0  13685  hashf  13686  hash0  13716  prhash2ex  13748  hashsslei  13775  hashxplem  13782  hashbclem  13798  hashf1lem1  13801  wrdexgOLD  13860  s1dm  13950  eqs1  13954  ccat2s1p1  13973  cats1un  14071  revs1  14115  0csh0  14143  cshw1  14172  cats1fvn  14208  funcnvs1  14262  pfx2  14297  relexp0g  14369  relexpsucnnr  14372  dfrtrclrec2  14404  rtrclreclem1  14405  rtrclreclem2  14406  rtrclreclem4  14408  dfrtrcl2  14409  climmo  14902  fsumcom2  15117  ackbijnn  15171  incexclem  15179  infcvgaux1i  15200  fprodcom2  15326  bpolylem  15390  bpoly3  15400  bpoly4  15401  efcvgfsum  15427  cos1bnd  15528  cos2bnd  15529  znnen  15553  qnnen  15554  aleph1re  15586  3dvds  15668  n2dvdsm1  15707  n2dvds3OLD  15710  divalglem5  15736  flodddiv4  15752  sadcaddlem  15794  sadadd2lem  15796  sadadd3  15798  sadaddlem  15803  lcmf0  15966  lcmfunsnlem2lem1  15970  lcmfunsnlem2  15972  coprmprod  15993  coprmproddvdslem  15994  2prm  16024  3lcm2e6  16060  phicl2  16093  pockthi  16231  unbenlem  16232  prmrec  16246  vdwlem13  16317  vdwnn  16322  ramcl2  16340  prmgapprmo  16386  mod2xnegi  16395  modsubi  16396  structcnvcnv  16485  setsres  16513  strfv  16519  strleun  16579  0rest  16691  firest  16694  restid  16695  prdsval  16716  prdsbas  16718  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  imasaddfnlem  16789  imasvscafn  16798  oppchomfval  16972  oppcbas  16976  2oppchomf  16982  rescbas  17087  rescco  17090  rescabs  17091  0ssc  17095  0subcat  17096  idfucl  17139  homarel  17284  dmaf  17297  cdaf  17298  catcfuccl  17357  relxpchom  17419  catcxpccl  17445  oppchofcl  17498  oyoncl  17508  odubas  17731  letsr  17825  mgmidmo  17858  pwmnd  18040  releqg  18265  ga0  18366  oppglem  18416  psgnunilem3  18553  psgnunilem4  18554  pmtrsn  18576  efgval  18772  efger  18773  efgsval2  18788  efgsp1  18792  efgsfo  18794  efgredleme  18798  efgredlem  18802  efgred  18803  cygctb  18941  gsum2d2lem  19022  gsum2d2  19023  gsumcom2  19024  dprd2d2  19095  pgpfaclem1  19132  mgplem  19173  mgpress  19179  opprlem  19307  reldvdsr  19323  00lsp  19682  sralem  19878  srasca  19882  sravsca  19883  psrvscafval  20098  opsrbaslem  20186  psrbag0  20202  00ply1bas  20336  ply1plusgfvi  20338  cnfldfun  20485  cnfldfunALT  20486  xrsmgm  20508  zlmsca  20596  znbaslem  20613  resubdrg  20680  ocv0  20749  cssval  20754  thlbas  20768  thlle  20769  islinds2  20885  matsca  20952  m2detleib  21168  tgdom  21514  tgidm  21516  indistps2ALT  21550  restbas  21694  resttopon  21697  rest0  21705  leordtval2  21748  iocpnfordt  21751  icomnfordt  21752  iooordt  21753  ist1-3  21885  1stcfb  21981  comppfsc  22068  1stckgen  22090  ptbasfi  22117  dfac14  22154  opnfbas  22378  hauspwpwf1  22523  alexsubALT  22587  ptcmplem5  22592  cnextrel  22599  ust0  22755  tuslem  22803  0met  22903  prdsdsf  22904  prdsxmetlem  22905  prdsmet  22907  setsmsbas  23012  setsmsds  23013  prdsbl  23028  tngds  23184  qtopbaslem  23294  xrtgioo  23341  xrsdsre  23345  zcld  23348  recld2  23349  reperflem  23353  retopconn  23364  iccpnfcnv  23475  bndth  23489  nmoleub2lem2  23647  zclmncvs  23679  recmet  23853  resscdrg  23888  ishl2  23900  recms  23910  volf  24057  iundisj2  24077  volsup  24084  icombl  24092  ioombl  24093  ismbf3d  24182  0plef  24200  0pledm  24201  itg1ge0  24214  mbfi1fseqlem5  24247  itg2addlem  24286  reldv  24395  limciun  24419  dvexp  24477  dveflem  24503  lhop1lem  24537  lhop  24540  elply2  24713  elplyd  24719  ply1term  24721  ply0  24725  plymullem  24733  qaa  24839  pserulm  24937  pserdvlem2  24943  efcn  24958  sincosq1lem  25010  tangtx  25018  sincos4thpi  25026  pigt3  25030  pige3ALT  25032  efif1olem4  25056  logf1o  25075  relogf1o  25077  log1  25096  loge  25097  relogiso  25108  dvrelog  25147  relogcn  25148  logcn  25157  cxpcn3  25256  resqrtcn  25257  2logb9irr  25300  leibpi  25447  log2ublem1  25451  birthday  25459  emcllem5  25504  harmonicbnd  25508  harmonicbnd2  25509  harmonicbnd3  25512  lgamgulm2  25540  lgamcvglem  25544  gamf  25547  ppiltx  25681  ppiublem1  25705  ppiub  25707  bclbnd  25783  bpos1lem  25785  bposlem8  25794  lgsquadlem2  25884  2sqlem9  25930  2sqlem10  25931  addsqnreup  25946  chebbnd1  25975  selberg2lem  26053  pntrsumo1  26068  selbergsb  26078  pntpbnd  26091  istrkg2ld  26173  tgcgr4  26244  ttgval  26588  ttglem  26589  cchhllem  26600  ax5seglem7  26648  axlowdimlem4  26658  axlowdimlem6  26660  axlowdimlem7  26661  axlowdimlem10  26664  axlowdimlem13  26667  axlowdimlem16  26670  uhgr0e  26783  uhgr0  26785  upgrbi  26805  umgrbi  26813  usgr0  26952  lfuhgr1v0e  26963  usgrexmpllem  26969  usgrexmpl  26972  griedg0prc  26973  cplgr0  27134  usgrexilem  27149  cffldtocusgr  27156  rgrusgrprc  27298  rusgrprc  27299  rgrprcx  27301  rgrx0ndm  27302  usgr2pthlem  27471  pthdlem2  27476  uspgrn2crct  27513  wwlksnext  27598  wwlksnfi  27611  wwlksnfiOLD  27612  disjxwwlkn  27619  clwwlknondisj  27817  0ewlk  27820  0wlk  27822  0pth  27831  1pthdlem1  27841  1trld  27848  wlk2v2elem2  27862  wlk2v2e  27863  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  dfconngr1  27894  0conngr  27898  konigsbergumgr  27957  2wspmdisj  28043  2clwwlk2clwwlk  28056  numclwwlk3lem2lem  28089  numclwwlk3lem2  28090  ex-dif  28129  ex-in  28131  ex-eprel  28139  ex-id  28140  ex-fl  28153  ex-mod  28155  ex-hash  28159  ex-fpar  28168  avril1  28169  2bornot2b  28170  0vfval  28310  vsfval  28337  ajmoi  28562  ajfuni  28563  normlem2  28815  norm3adifii  28852  hhip  28881  hlim0  28939  hlimcaui  28940  hlimf  28941  hhssnv  28968  shscli  29021  shsval2i  29091  h1de2i  29257  fh3i  29327  fh4i  29328  cm2mi  29330  qlaxr3i  29340  mayetes3i  29433  ho0f  29455  hoif  29458  hodidi  29491  ho0subi  29499  hosd1i  29526  adjmo  29536  nmopsetn0  29569  nmfnsetn0  29582  funadj  29590  funcnvadj  29597  nmcexi  29730  cnlnadjlem8  29778  nmoptri2i  29803  opsqrlem4  29847  hmopidmchi  29855  pjoci  29884  pjinvari  29895  abrexdomjm  30194  elim2ifim  30227  iundisj2f  30268  rinvf1o  30303  dfcnv2  30350  snct  30375  fzodif2  30441  iundisj2fi  30446  dp2lt10  30487  dp2ltc  30490  dplti  30508  dpgti  30509  dpexpp1  30511  gsumle  30652  xrge0slmod  30844  xrge0pluscn  31082  zlmds  31104  zlmtset  31105  qqhre  31160  esumrnmpt2  31226  esumfsup  31228  esumpcvgval  31236  hasheuni  31243  esumcvg  31244  esumcvgsum  31246  esumsup  31247  esum2d  31251  dmsigagen  31302  ldgenpisyslem3  31323  measvuni  31372  voliune  31387  volfiniune  31388  br2base  31426  dya2iocuni  31440  eulerpartlem1  31524  eulerpartlemt  31528  eulerpartgbij  31529  fib0  31556  coinfliprv  31639  ballotlem2  31645  ballotlemic  31663  ballotlem7  31692  ballotth  31694  plymul02  31715  rpsqrtcn  31763  chtvalz  31799  circlemethnat  31811  circlevma  31812  circlemethhgt  31813  hgt750lem  31821  bnj226  31903  bnj1101  31955  bnj110  32029  bnj149  32046  bnj150  32047  bnj151  32048  bnj517  32056  bnj580  32084  bnj865  32094  bnj900  32100  bnj996  32126  bnj1110  32151  bnj1133  32158  bnj1128  32159  bnj1145  32162  bnj1137  32164  bnj1171  32169  bnj1176  32174  f1resfz0f1d  32258  subfacp1lem5  32328  subfacp1lem6  32329  kur14lem9  32358  cvmcov2  32419  cvmliftlem1  32429  cvmliftlem4  32432  cvmliftlem5  32433  gonanegoal  32496  satfv0  32502  satfv0fun  32515  fmlan0  32535  gonan0  32536  fmla0disjsuc  32542  ex-sategoelel12  32571  msrfo  32690  problem5  32809  brtpid1  32848  brtpid2  32849  brtpid3  32850  logi  32863  faclimlem1  32872  axextndbi  32946  poseq  32992  sltval2  33060  noxp1o  33067  nosepnelem  33081  txprel  33237  relsset  33246  relbigcup  33255  fvbigcup  33260  fnsingle  33277  fvsingle  33278  snelsingles  33280  funimage  33286  fullfunfnv  33304  imagesset  33311  funtransport  33389  colinrel  33415  funray  33498  funline  33500  0hf  33535  neibastop2lem  33605  filnetlem3  33625  nrmo  33655  waj-ax  33659  lukshef-ax2  33660  arg-ax  33661  limsucncmpi  33690  dnizeq0  33711  knoppcnlem8  33736  knoppcnlem11  33739  cnndvlem1  33773  bj-babylob  33835  bj-ax12ssb  33888  bj-nnfnth  33969  bj-disjcsn  34160  bj-snsetex  34172  bj-0eltag  34187  bj-2upln0  34232  bj-2upln1upl  34233  bj-isrvec  34463  f1omptsnlem  34499  f1omptsn  34500  icoreresf  34515  relowlssretop  34526  relowlpssretop  34527  domalom  34567  matunitlindf  34771  poimirlem3  34776  poimirlem9  34782  poimirlem16  34789  poimirlem17  34790  poimirlem18  34791  poimirlem19  34792  poimirlem20  34793  poimirlem26  34799  mblfinlem1  34810  mblfinlem2  34811  ismblfin  34814  voliunnfl  34817  cnambfre  34821  abrexdom  34886  fdc  34901  cncfres  34924  heibor1lem  34968  grposnOLD  35041  bicontr  35239  an12i  35257  tsim1  35289  ac6s6f  35332  vvdifopab  35402  brcnvrabga  35480  opabf  35500  xrnrel  35505  relcoels  35549  cnvcosseq  35562  refrelcoss3  35583  refrelcoss2  35584  symrelcoss2  35586  refrelcoss  35642  symrelcoss  35676  n0eldmqs  35763  ax13fromc9  35922  dedths  35978  renegclALT  35979  hlhilslem  38954  sn-axprlem3  38987  rtprmirr  39072  dffltz  39149  moxfr  39167  mapfzcons1  39192  diophrw  39234  0dioph  39253  vdioph  39254  rabren3dioph  39290  2nn0ind  39420  rpnnen3  39507  kelac2lem  39542  frlmpwfi  39576  ifpbiidcor2  39727  iscard4  39778  eliunov2  39902  xphe  40005  0he  40006  he0  40008  snhesn  40010  idhe  40011  frege54cor1c  40139  clsk1independent  40274  neicvgnvor  40344  amgm2d  40429  amgm3d  40430  amgm4d  40431  lhe4.4ex1a  40538  rusbcALT  40648  ipo0  40658  ifr0  40659  vk15.4j  40739  2sb5nd  40771  dfvd1ir  40784  dfvd2anir  40795  dfvd2ir  40797  dfvd3ir  40804  dfvd3anir  40807  iden2  40825  e0bir  40988  uun2221p1  41025  uun2221p2  41026  2sb5ndVD  41121  2sb5ndALT  41143  iunconnlem2  41146  fnchoice  41163  unisn0  41193  eliincex  41253  icof  41358  supminfxr  41616  fsumiunss  41732  climlimsupcex  41926  liminfltlimsupex  41938  liminflelimsupcex  41954  xlimrel  41977  xlimfun  42012  resincncf  42034  dvnprodlem3  42109  volioc  42133  volico  42145  dmvolss  42147  volioof  42149  stoweidlem13  42175  stoweidlem34  42196  stirlinglem5  42240  stirlinglem13  42248  stirlingr  42252  fourierdlem42  42311  fourierdlem62  42330  fouriersw  42393  etransc  42445  salexct  42494  salexct2  42499  salgencntex  42503  sge0rnn0  42527  gsumge0cl  42530  sge00  42535  sge0resplit  42565  sge0reuz  42606  omeiunle  42676  0ome  42688  icoresmbl  42702  ovn0lem  42724  ovnhoilem1  42760  hspmbl  42788  ovolval5lem3  42813  nsssmfmbf  42932  mbfpsssmf  42936  smfresal  42940  smfmullem4  42946  smfpimbor1lem1  42950  smfpimbor1lem2  42951  aistia  43010  aisfina  43011  aiffnbandciffatnotciffb  43017  axorbciffatcxorb  43018  abnotbtaxb  43028  abnotataxb  43029  eusnsn  43138  aiotaval  43170  aiota0ndef  43172  fundcmpsurinjimaid  43448  ichv  43486  ichf  43487  ichid  43488  ichcircshi  43489  icheq  43497  spr0nelg  43515  m3prm  43631  m7prm  43641  0noddALTV  43731  2noddALTV  43735  341fppr2  43776  9fppr8  43779  nfermltl8rev  43784  nfermltl2rev  43785  nfermltlrev  43786  sbgoldbo  43829  nnsum3primes4  43830  evengpop3  43840  oddinmgm  43959  nn0mnd  43963  efmndmgm  43982  smndex1ibas  44000  smndex1mgm  44007  smndex1mnd  44010  smndex2dbas  44014  smndex2dnrinv  44015  smndex2hbas  44016  2zrngamgm  44138  2zrngaabl  44143  2zrngmmgm  44145  2zrngnring  44151  fldhmsubc  44283  fldhmsubcALTV  44301  eliunxp2  44310  zlmodzxzldeplem  44481  zlmodzxzldep  44487  ldepslinc  44492  rrx2xpreen  44634  rrx2plordisom  44638  line2ylem  44666  line2  44667  line2x  44669  inlinecirc02plem  44701  ex-gte  44756  empty-surprise  44811  eximp-surprise2  44814  amgmw2d  44833
  Copyright terms: Public domain W3C validator