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  310  orri  390  imorri  429  imnani  438  mpbir2an  975  mpbir3an  1263  xorexmid  1520  tru  1527  had1  1582  nic-mpALT  1637  nic-ax  1638  nic-axALT  1639  nfi  1754  mpgbir  1766  nfxfr  1819  19.35ri  1847  nfxfrOLD  1877  ax5e  1881  ax6ev  1947  exanOLDOLD  2205  ax13  2285  ax13ALT  2341  euequ1  2504  moanmo  2561  axi12  2629  axext2  2632  eqeltri  2726  nfcxfr  2791  neir  2826  neirr  2832  eqnetri  2893  nelir  2929  mprgbir  2956  vex  3234  issetri  3241  moeq  3415  rmoeq  3438  cdeqi  3453  eqsstri  3668  3sstr4i  3677  rabnc  3995  tpid1  4335  tpid2  4336  pwv  4465  uni0  4497  int0  4522  eqbrtri  4706  tr0  4797  trv  4798  zfrep4  4812  zfnuleu  4819  axnulALT  4820  0ex  4823  inex1  4832  elpwi2  4859  0elpw  4864  axpow2  4875  axpow3  4876  pwex  4878  dvdemo1  4932  zfpair2  4937  exss  4961  brv  4970  opwo0id  4990  moop2  4995  pwundif  5050  po0  5079  epse  5126  relxp  5160  relsnopOLD  5262  rel0  5276  relopabi  5278  relopabiALT  5279  eliunxp  5292  opeliunxp2  5293  dmi  5372  xpidtr  5553  xpima  5611  cnvcnv  5621  cnvcnvOLD  5622  dmsn0  5637  cnvsn0  5638  0elon  5816  funmpt  5964  funmpt2  5965  funcnv0  5993  isarep2  6016  fresaunres2  6114  f0  6124  f10  6207  f10d  6208  f1o00  6209  f1oi  6212  f1osn  6214  brprcneu  6222  opabiotafun  6298  fvopab3ig  6317  opabex  6524  mptexgf  6526  eufnfv  6531  isof1oopb  6615  canth  6648  ncanth  6649  mpt2fun  6804  reldmmpt2  6813  ovid  6819  ovidig  6820  ovidi  6821  ovig  6824  ov3  6839  caovmo  6913  relmptopab  6925  porpss  6983  uniex2  6994  snnexOLD  7009  tfinds2  7105  finds  7134  finds2  7136  oprabex  7198  oprabex3  7199  f1stres  7234  f2ndres  7235  relmpt2opab  7304  opeliunxp2f  7381  tpos0  7427  wfrrel  7465  wfrlem14  7473  wfrlem16  7475  issmo  7490  tfrlem6  7523  tfrlem8  7525  tfrlem16  7534  tfr1a  7535  tfr1  7538  tz7.44lem1  7546  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  fnseqom  7595  0lt1o  7629  0we1  7631  eqer  7822  ecopover  7894  mapsnf1o3  7948  ssdomg  8043  ensn1  8061  snfi  8079  xpcomf1o  8090  map2xp  8171  limensuci  8177  sdom1  8201  unblem4  8256  fidomdm  8284  marypha1lem  8380  hartogslem1  8488  hartogs  8490  card2on  8500  ruALT  8546  inf2  8558  inf3lem6  8568  infeq5i  8571  zfinf2  8577  cantnflt  8607  cnfcom  8635  trcl  8642  tz9.1c  8644  tc2  8656  r1funlim  8667  r1fnon  8668  karden  8796  tskwe  8814  cardprclem  8843  pm54.43  8864  r0weon  8873  iunmapdisj  8884  alephfnon  8926  alephfplem4  8968  alephfp  8969  alephval3  8971  aceq3lem  8981  kmlem2  9011  cda1dif  9036  ackbij1  9098  ackbij2lem2  9100  ackbij2  9103  infpssrlem3  9165  hsmexlem4  9289  hsmexlem5  9290  axdc3lem4  9313  ac2  9321  axac3  9324  ac6  9340  axdclem2  9380  dmct  9384  ondomon  9423  alephsucpw  9430  pwcfsdom  9443  cfpwsdom  9444  smobeth  9446  axpowndlem3  9459  zfcndun  9475  zfcndpow  9476  zfcndinf  9478  zfcndac  9479  wunex2  9598  uniwun  9600  wuncval2  9607  grur1  9680  axgroth5  9684  axgroth2  9685  axgroth6  9688  axgroth3  9691  grothtsk  9695  inaprc  9696  ltsopi  9748  dmaddpi  9750  dmmulpi  9751  1lt2pi  9765  nqerf  9790  addnqf  9808  mulnqf  9809  1lt2nq  9833  m1p1sr  9951  m1m1sr  9952  0lt1sr  9954  axaddf  10004  axmulf  10005  ax1cn  10008  subaddrii  10408  ixi  10694  recgt0ii  10967  nn1suc  11079  neg1lt0  11165  4d2e2  11222  arch  11327  un0mulcl  11365  pnf0xnn0  11408  3halfnz  11494  nummac  11596  uzf  11728  indstr  11794  mnfltpnf  11998  ixxf  12223  ioof  12309  fzf  12368  0nelfz1  12398  fzp1disj  12437  fzp1nel  12462  fzof  12506  om2uzrani  12791  om2uzf1oi  12792  uzrdglem  12796  uzrdgfni  12797  uzrdg0i  12798  ltwenn  12801  hashgf1o  12810  axdc4uzlem  12822  sq0  12995  irec  13004  facmapnn  13112  hashkf  13159  hashfxnn0  13164  hashf  13165  hashfOLD  13166  hash0  13196  prhash2ex  13225  hashsslei  13251  hashxplem  13258  hashbclem  13274  hashf1lem1  13277  wrdexg  13347  s1dm  13425  revs1  13560  0csh0  13585  cshw1  13614  cats1fvn  13649  s2dm  13681  funcnvs1  13703  relexp0g  13806  relexpsucnnr  13809  dfrtrclrec2  13841  rtrclreclem1  13842  rtrclreclem2  13843  rtrclreclem4  13845  dfrtrcl2  13846  climmo  14332  fsumcom2  14549  fsumcom2OLD  14550  ackbijnn  14604  incexclem  14612  infcvgaux1i  14633  fprodcom2  14758  fprodcom2OLD  14759  fprodn0f  14766  fprodge0  14768  fprodge1  14770  bpolylem  14823  bpoly3  14833  bpoly4  14834  efcvgfsum  14860  cos1bnd  14961  cos2bnd  14962  znnen  14985  qnnen  14986  aleph1re  15018  3dvds  15099  3dvdsOLD  15100  n2dvdsm1  15152  n2dvds3  15154  divalglem5  15167  flodddiv4  15184  bitsf  15196  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  lcmf0  15394  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  coprmprod  15422  coprmproddvdslem  15423  2prm  15452  3lcm2e6  15487  phicl2  15520  pockthi  15658  unbenlem  15659  prmrec  15673  vdwlem13  15744  vdwnn  15749  ramcl2  15767  prmgapprmo  15813  mod2xnegi  15822  modsubi  15823  prmo4  15882  prmo5  15883  prmo6  15884  structcnvcnv  15918  setsres  15948  strfv  15954  strlemor1OLD  16016  strleun  16019  0rest  16137  firest  16140  restid  16141  prdsval  16162  prdsbas  16164  prdsplusg  16165  prdsmulr  16166  prdsvsca  16167  prdsds  16171  imasaddfnlem  16235  imasvscafn  16244  oppchomfval  16421  oppcbas  16425  2oppchomf  16431  rescbas  16536  rescco  16539  rescabs  16540  0ssc  16544  0subcat  16545  idfucl  16588  wunnat  16663  homarel  16733  dmaf  16746  cdaf  16747  catcfuccl  16806  relxpchom  16868  catcxpccl  16894  oppchofcl  16947  oyoncl  16957  odubas  17180  letsr  17274  mgmidmo  17306  releqg  17688  ga0  17777  oppglem  17826  psgnunilem3  17962  psgnunilem4  17963  pmtrsn  17985  efgval  18176  efger  18177  efgsp1  18196  efgsfo  18198  efgredleme  18202  efgredlem  18206  efgred  18207  cygctb  18339  gsum2d2lem  18418  gsum2d2  18419  gsumcom2  18420  dprd2d2  18489  pgpfaclem1  18526  mgplem  18540  mgpress  18546  opprlem  18674  reldvdsr  18690  00lsp  19029  sralem  19225  srasca  19229  sravsca  19230  psrvscafval  19438  opsrbaslem  19525  opsrbaslemOLD  19526  psrbag0  19542  00ply1bas  19658  ply1plusgfvi  19660  cnfldfun  19806  cnfldfunALT  19807  xrsmgm  19829  zlmsca  19917  znbaslem  19934  znbaslemOLD  19935  resubdrg  20002  ocvfval  20058  ocv0  20069  cssval  20074  thlbas  20088  thlle  20089  islinds2  20200  matsca  20269  m2detleib  20485  tgdom  20830  tgidm  20832  indistps2ALT  20866  restbas  21010  resttopon  21013  rest0  21021  leordtval2  21064  iocpnfordt  21067  icomnfordt  21068  iooordt  21069  cnpfval  21086  iscnp2  21091  ist1-3  21201  1stcfb  21296  islly2  21335  comppfsc  21383  1stckgen  21405  ptbasfi  21432  xkotf  21436  dfac14  21469  opnfbas  21693  hauspwpwf1  21838  alexsubALTlem4  21901  alexsubALT  21902  ptcmplem5  21907  cnextrel  21914  ust0  22070  tuslem  22118  0met  22218  prdsdsf  22219  prdsxmetlem  22220  prdsmet  22222  setsmsbas  22327  setsmsds  22328  prdsbl  22343  tngds  22499  qtopbaslem  22609  xrtgioo  22656  xrsdsre  22660  zcld  22663  recld2  22664  sszcld  22667  reperflem  22668  retopconn  22679  iccpnfcnv  22790  bndth  22804  ishtpy  22818  nmoleub2lem2  22962  zclmncvs  22994  recmet  23166  resscdrg  23200  ishl2  23212  recms  23214  volf  23343  iundisj2  23363  volsup  23370  icombl  23378  ioombl  23379  ismbf3d  23466  0plef  23484  0pledm  23485  itg1ge0  23498  mbfi1fseqlem5  23531  itg2addlem  23570  iblcnlem1  23599  reldv  23679  limciun  23703  dvexp  23761  dveflem  23787  lhop1lem  23821  lhop  23824  elply2  23997  elplyd  24003  ply1term  24005  ply0  24009  plymullem  24017  qaa  24123  pserulm  24221  pserdvlem2  24227  efcn  24242  sincosq1lem  24294  tangtx  24302  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  efif1olem4  24336  logf1o  24356  relogf1o  24358  log1  24377  loge  24378  relogiso  24389  dvrelog  24428  relogcn  24429  logcn  24438  cxpcn3  24534  resqrtcn  24535  leibpi  24714  log2ublem1  24718  birthday  24726  emcllem5  24771  harmonicbnd  24775  harmonicbnd2  24776  emgt0  24778  harmonicbnd3  24779  lgamgulm2  24807  lgamcvglem  24811  gamf  24814  ppiltx  24948  ppiublem1  24972  ppiub  24974  bclbnd  25050  bpos1lem  25052  bposlem8  25061  lgsquadlem2  25151  2sqlem9  25197  2sqlem10  25198  chebbnd1  25206  selberg2lem  25284  pntrsumo1  25299  selbergsb  25309  pntpbnd  25322  istrkg2ld  25404  tgcgr4  25471  ttgval  25800  ttglem  25801  cchhllem  25812  ax5seglem7  25860  axlowdimlem4  25870  axlowdimlem6  25872  axlowdimlem7  25873  axlowdimlem10  25876  axlowdimlem13  25879  axlowdimlem16  25882  uhgr0e  26011  uhgr0  26013  upgrbi  26033  umgrbi  26041  usgr0  26180  lfuhgr1v0e  26191  usgrexmpllem  26197  usgrexmpl  26200  griedg0prc  26201  cplgr0  26377  usgrexilem  26392  cffldtocusgr  26399  rgrusgrprc  26541  rusgrprc  26542  rgrprcx  26544  rgrx0ndm  26545  usgr2pthlem  26715  pthdlem2  26720  uspgrn2crct  26756  wwlksnext  26856  wwlksnfi  26869  disjxwwlkn  26876  clwwlknondisj  27086  clwwlknondisjOLD  27090  0ewlk  27092  0wlk  27094  0pth  27103  1pthdlem1  27113  1trld  27120  wlk2v2elem2  27134  wlk2v2e  27135  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  dfconngr1  27166  0conngr  27170  konigsbergumgr  27229  2wspmdisj  27317  2clwwlk2clwwlk  27338  numclwwlk3lemOLD  27369  numclwwlk3lemlem  27370  numclwwlk3lem  27371  ex-dif  27410  ex-in  27412  ex-eprel  27420  ex-id  27421  ex-fl  27434  ex-mod  27436  ex-hash  27440  avril1  27449  2bornot2b  27450  0vfval  27589  vsfval  27616  ajmoi  27842  ajfuni  27843  normlem2  28096  norm3adifii  28133  hhip  28162  hlim0  28220  hlimcaui  28221  hlimf  28222  hhssnv  28249  shscli  28304  shsval2i  28374  h1de2i  28540  fh3i  28610  fh4i  28611  cm2mi  28613  qlaxr3i  28623  mayetes3i  28716  ho0f  28738  hoif  28741  hodidi  28774  ho0subi  28782  hosd1i  28809  adjmo  28819  nmopsetn0  28852  nmfnsetn0  28865  funadj  28873  funcnvadj  28880  nmcexi  29013  cnlnadjlem8  29061  nmoptri2i  29086  opsqrlem4  29130  hmopidmchi  29138  pjoci  29167  pjinvari  29178  abrexdomjm  29471  elim2ifim  29490  iundisj2f  29529  rinvf1o  29560  funcnvmptOLD  29595  dfcnv2  29604  snct  29619  fpwrelmap  29636  fzodif2  29680  iundisj2fi  29684  dp2lt10  29719  dp2ltc  29722  dplti  29741  dpgti  29742  dpexpp1  29744  gsumle  29907  xrge0slmod  29972  xrge0pluscn  30114  zlmds  30136  zlmtset  30137  qqhre  30192  esumrnmpt2  30258  esumfsup  30260  esumpcvgval  30268  hasheuni  30275  esumcvg  30276  esumcvgsum  30278  esumsup  30279  esum2d  30283  dmsigagen  30335  ldgenpisyslem3  30356  measvuni  30405  voliune  30420  volfiniune  30421  br2base  30459  dya2iocuni  30473  eulerpartlem1  30557  eulerpartlemt  30561  eulerpartgbij  30562  fib0  30589  coinfliprv  30672  ballotlem2  30678  ballotlemic  30696  ballotlem7  30725  ballotth  30727  plymul02  30751  rpsqrtcn  30799  chtvalz  30835  circlemethnat  30847  circlevma  30848  circlemethhgt  30849  hgt750lem  30857  bnj226  30928  bnj1101  30981  bnj110  31054  bnj149  31071  bnj150  31072  bnj151  31073  bnj517  31081  bnj580  31109  bnj865  31119  bnj900  31125  bnj996  31151  bnj1110  31176  bnj1133  31183  bnj1128  31184  bnj1145  31187  bnj1137  31189  bnj1171  31194  bnj1176  31199  subfacp1lem5  31292  subfacp1lem6  31293  kur14lem9  31322  cvmcov2  31383  cvmliftlem1  31393  cvmliftlem4  31396  cvmliftlem5  31397  msrfo  31569  problem5  31689  brtpid1  31728  brtpid2  31729  brtpid3  31730  logi  31746  faclimlem1  31755  domep  31822  axextndbi  31834  poseq  31878  frrlem6  31914  frrlem10  31916  sltval2  31934  noxp1o  31941  nosepnelem  31955  txprel  32111  relsset  32120  relbigcup  32129  fvbigcup  32134  fnsingle  32151  fvsingle  32152  snelsingles  32154  funimage  32160  fullfunfnv  32178  imagesset  32185  funtransport  32263  colinrel  32289  funray  32372  funline  32374  0hf  32409  neibastop2lem  32480  filnetlem3  32500  waj-ax  32538  lukshef-ax2  32539  arg-ax  32540  limsucncmpi  32569  dnizeq0  32590  knoppcnlem8  32615  knoppcnlem11  32618  cnndvlem1  32653  bj-babylob  32714  bj-ax12ssb  32760  bj-dvdemo1  32927  bj-disjcsn  33061  bj-snsetex  33076  bj-0eltag  33091  bj-2upln0  33136  bj-2upln1upl  33137  f1omptsnlem  33313  f1omptsn  33314  icoreresf  33330  relowlssretop  33341  relowlpssretop  33342  pigt3  33532  matunitlindf  33537  poimirlem3  33542  poimirlem9  33548  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem26  33565  mblfinlem1  33576  mblfinlem2  33577  ismblfin  33580  voliunnfl  33583  cnambfre  33588  cover2  33638  abrexdom  33655  fdc  33671  cncfres  33694  heibor1lem  33738  grposnOLD  33811  bicontr  34009  an12i  34030  tsim1  34067  ac6s6f  34111  vvdifopab  34165  opabf  34270  xrnrel  34275  relcoels  34319  cnvcosseq  34332  refrelcoss3  34353  refrelcoss2  34354  symrelcoss2  34356  refrelcoss  34412  symrelcoss  34446  ax13fromc9  34510  dedths  34566  renegclALT  34567  hlhilslem  37547  moxfr  37572  mapfzcons1  37597  diophrw  37639  0dioph  37659  vdioph  37660  rabren3dioph  37696  2nn0ind  37827  rpnnen3  37916  kelac2lem  37951  frlmpwfi  37985  ifpbiidcor2  38145  relintabex  38204  eliunov2  38288  xphe  38392  0he  38393  he0  38395  snhesn  38397  idhe  38398  frege54cor1c  38526  clsk1independent  38661  neicvgnvor  38731  amgm2d  38818  amgm3d  38819  amgm4d  38820  lhe4.4ex1a  38845  rusbcALT  38957  ipo0  38970  ifr0  38971  vk15.4j  39051  2sb5nd  39093  dfvd1ir  39106  dfvd2anir  39117  dfvd2ir  39119  dfvd3ir  39126  dfvd3anir  39129  iden2  39156  e0bir  39321  uun2221p1  39358  uun2221p2  39359  2sb5ndVD  39460  2sb5ndALT  39482  iunconnlem2  39485  fnchoice  39502  unisn0  39536  eliincex  39607  icof  39725  mptssid  39764  supminfxr  40007  fsumiunss  40125  climlimsupcex  40319  liminfltlimsupex  40331  liminflelimsupcex  40347  xlimrel  40364  resincncf  40406  dvnprodlem3  40481  mbf0  40491  volioc  40506  volico  40518  dmvolss  40520  volioof  40522  stoweidlem13  40548  stoweidlem34  40569  stirlinglem5  40613  stirlinglem13  40621  stirlingr  40625  fourierdlem42  40684  fourierdlem62  40703  fouriersw  40766  etransc  40818  salexct  40870  salexct2  40875  salgencntex  40879  sge0rnn0  40903  gsumge0cl  40906  sge00  40911  sge0resplit  40941  sge0reuz  40982  omeiunle  41052  0ome  41064  icoresmbl  41078  ovn0lem  41100  ovnhoilem1  41136  hspmbl  41164  ovolval5lem3  41189  nsssmfmbf  41308  mbfpsssmf  41312  smfresal  41316  smfmullem4  41322  smfpimbor1lem1  41326  smfpimbor1lem2  41327  aistia  41385  aisfina  41386  aiffnbandciffatnotciffb  41392  axorbciffatcxorb  41393  abnotbtaxb  41403  abnotataxb  41404  pfx2  41737  m3prm  41831  m7prm  41841  0noddALTV  41925  2noddALTV  41929  sbgoldbo  42000  nnsum3primes4  42001  evengpop3  42011  spr0nelg  42051  oddinmgm  42140  2zrngamgm  42264  2zrngaabl  42269  2zrngmmgm  42271  2zrngnring  42277  fldhmsubc  42409  fldhmsubcALTV  42427  eliunxp2  42437  zlmodzxzldeplem  42612  zlmodzxzldep  42618  ldepslinc  42623  ex-gte  42798  empty-surprise  42856  eximp-surprise2  42859  amgmw2d  42878
  Copyright terms: Public domain W3C validator