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

Theorem mpbir 202
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
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 199 . 2
41, 3ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  <->wb 178
This theorem is referenced by:  pm5.74ri  239  con4bii  290  orri  367  imorri  405  imnani  414  mpbir2an  888  mpbir3an  1144  xorexmid  1334  tru  1340  nic-mpALT  1457  nic-ax  1458  nic-axALT  1459  mtp-xor  1555  mpgbir  1574  nfxfr  1594  19.35ri  1630  a6ev  1687  exan  1907  cbval2OLD  1997  cbvex2  1998  ax13  2025  a6eOLD  2039  sbtOLD  2136  moanmo  2388  moaneuOLD  2390  axi12  2468  axext2  2471  eqeltri  2559  nfcxfr  2622  neir  2657  neirr  2659  exmidne  2660  eqnetri  2671  nesymir  2695  nelir  2752  mprgbir  2830  vex  3018  issetri  3022  moeq  3173  cdeqi  3209  eqsstri  3423  3sstr4i  3432  tpid1  4017  tpid2  4018  tpid3  4020  pwv  4116  uni0  4144  eqbrtri  4337  tr0  4422  trv  4423  zfrep4  4437  zfnuleu  4444  axnulALT  4445  0ex  4448  inex1  4459  0elpw  4484  axpow2  4495  axpow3  4496  pwex  4498  dvdemo1  4550  zfpair2  4555  exss  4578  moop2  4608  pwundif  4649  po0  4677  epse  4724  0elon  4793  relsnop  4966  relxp  4969  rel0  4986  relopabi  4987  eliunxp  4999  opeliunxp2  5000  dmi  5076  xpidtr  5243  xpima  5301  cnvcnv  5310  dmsn0  5326  cnvsn0  5327  funmpt  5474  funmpt2  5475  isarep2  5516  fresaunres2  5600  f0  5609  f10  5689  f1o00  5690  f1oi  5693  f1osn  5695  brprcneu  5701  opabiotafun  5768  fvopab3ig  5787  opabex  5961  eufnfv  5965  canth  6059  ncanth  6060  mpt2fun  6204  reldmmpt2  6213  ovid  6218  ovidig  6219  ovidi  6220  ovig  6223  ov3  6238  caovmo  6310  relmptopab  6318  porpss  6374  uniex2  6385  snnex  6392  tfinds2  6484  finds  6512  finds2  6514  oprabex  6571  oprabex3  6572  f1stres  6604  f2ndres  6605  relmpt2opab  6661  tpos0  6741  issmo  6772  tfrlem6  6805  tfrlem8  6807  tfrlem16  6816  tfr1a  6817  tfr1  6820  tz7.44lem1  6825  seqomlem2  6870  seqomlem3  6871  seqomlem4  6872  fnseqom  6874  abianfp  6878  0lt1o  6910  0we1  6912  eqer  7100  ecopover  7170  th3qcor  7174  mapsnf1o3  7225  ssdomg  7317  ensn1  7335  snfi  7352  xpcomf1o  7362  map2xp  7442  limensuci  7448  sdom1  7473  unblem4  7528  fidomdm  7554  marypha1lem  7605  hartogslem1  7678  hartogs  7680  card2on  7689  ruALT  7736  inf2  7745  inf3lem6  7755  infeq5i  7758  zfinf2  7764  cantnflt  7794  cantnf  7816  mapfien  7820  cnfcom  7824  trcl  7831  tz9.1c  7833  tc2  7848  r1funlim  7859  r1fnon  7860  karden  7988  tskwe  8006  cardprclem  8035  pm54.43  8056  r0weon  8065  iunmapdisj  8075  alephfnon  8117  alephfplem4  8159  alephfp  8160  alephval3  8162  aceq3lem  8172  kmlem2  8202  cda1dif  8227  ackbij1  8289  ackbij2lem2  8291  ackbij2  8294  infpssrlem3  8356  hsmexlem4  8480  hsmexlem5  8481  axdc3lem4  8504  ac2  8512  axac3  8515  ac6  8531  axdclem2  8571  ondomon  8609  alephsucpw  8616  pwcfsdom  8629  cfpwsdom  8630  smobeth  8632  axpowndlem3  8645  zfcndun  8661  zfcndpow  8662  zfcndinf  8664  zfcndac  8665  wunex2  8784  uniwun  8786  wuncval2  8793  grur1  8866  axgroth5  8870  axgroth2  8871  axgroth6  8874  axgroth3  8877  grothtsk  8881  inaprc  8882  ltsopi  8936  dmaddpi  8938  dmmulpi  8939  1lt2pi  8953  nqerf  8978  addnqf  8996  mulnqf  8997  1lt2nq  9021  m1p1sr  9138  m1m1sr  9139  0lt1sr  9141  axaddf  9191  axmulf  9192  ax1cn  9195  subaddrii  9572  ixi  9838  recgt0ii  10104  nn1suc  10209  neg1lt0  10294  4d2e2  10344  arch  10442  un0mulcl  10480  nummac  10651  uzf  10728  indstr  10787  mnfltpnf  10970  ixxf  11174  ioof  11250  fzf  11297  fzp1disj  11368  fzof  11402  om2uzrani  11624  om2uzf1oi  11625  uzrdglem  11629  uzrdgfni  11630  uzrdg0i  11631  ltwenn  11634  hashgf1o  11642  axdc4uzlem  11653  sq0  11806  irec  11814  hashkf  11954  hashf  11959  hash0  11984  hashsslei  12025  hashxplem  12042  hashbclem  12052  hashf1lem1  12055  wrdexg  12091  wrd0  12099  revs1  12252  0csh0  12277  cshw1  12303  cats1fvn  12332  climmo  12882  fsumcom2  13089  ackbijnn  13138  incexclem  13146  infcvgaux1i  13166  efcvgfsum  13218  cos1bnd  13318  cos2bnd  13319  znnen  13342  qnnen  13343  aleph1re  13374  dvdslelem  13424  3dvds  13443  divalglem5  13448  bitsf  13470  sadcaddlem  13500  sadadd2lem  13502  sadadd3  13504  sadaddlem  13509  isprm3  13619  2prm  13626  phicl2  13690  pockthi  13815  unbenlem  13816  prmrec  13830  vdwlem13  13901  vdwnn  13906  ramcl2  13924  mod2xnegi  13947  modsubi  13948  structcnvcnv  14032  structfun  14033  setsres  14049  strfv  14055  strlemor1  14110  strleun  14113  0rest  14211  firest  14214  restid  14215  prdsval  14232  prdsbas  14234  prdsplusg  14235  prdsmulr  14236  prdsvsca  14237  prdsds  14240  imasaddfnlem  14307  imasvscafn  14316  oppchomfval  14494  oppcbas  14498  2oppchomf  14504  rescbas  14583  rescco  14586  rescabs  14587  idfucl  14632  wunnat  14707  homarel  14745  dmaf  14758  cdaf  14759  catcfuccl  14818  relxpchom  14832  catcxpccl  14858  oppchofcl  14911  oyoncl  14921  odubas  15144  letsr  15238  mgmidmo  15259  releqg  15558  ga0  15646  oppglem  15755  efgval  15958  efger  15959  efgsp1  15978  efgsfo  15980  efgredleme  15984  efgredlem  15988  efgred  15989  cygctb  16111  gsum2d2lem  16162  gsum2d2  16163  gsumcom2  16164  dprd2d2  16217  pgpfaclem1  16254  mgplem  16268  mgpress  16274  opprlem  16349  reldvdsr  16365  00lsp  16676  sralem  16872  srasca  16876  psrvscafval  17079  opsrbaslem  17163  psrbag0  17179  00ply1bas  17259  ply1plusgfvi  17261  zlmsca  17427  znbaslem  17444  ocvfval  17518  ocv0  17529  cssval  17534  thlbas  17548  thlle  17549  psgnunilem3  17649  psgnunilem4  17650  matsca  17786  m2detleib  17909  eltopspOLD  17997  tgdom  18057  tgidm  18059  indistps2ALT  18092  restbas  18236  resttopon  18239  rest0  18247  leordtval2  18290  iocpnfordt  18293  icomnfordt  18294  iooordt  18295  cnpfval  18312  iscnp2  18317  ist1-3  18427  1stcfb  18523  islly2  18562  1stckgen  18601  ptbasfi  18628  xkotf  18632  dfac14  18665  opnfbas  18889  hauspwpwf1  19034  alexsubALTlem4  19096  alexsubALT  19097  ptcmplem5  19102  cnextrel  19109  ust0  19264  tuslem  19312  0met  19411  prdsdsf  19412  prdsxmetlem  19413  prdsmet  19415  setsmsbas  19520  setsmsds  19521  prdsbl  19536  tngds  19704  qtopbaslem  19807  xrtgioo  19852  xrsdsre  19856  zcld  19859  recld2  19860  sszcld  19863  reperflem  19864  retopcon  19875  iccpnfcnv  19984  bndth  19998  ishtpy  20012  nmoleub2lem2  20139  recmet  20291  resscdrg  20327  ishl2  20339  volf  20440  iundisj2  20458  volsup  20465  icombl  20473  ioombl  20474  ismbf3d  20559  0plef  20577  0pledm  20578  itg1ge0  20591  mbfi1fseqlem5  20624  itg2addlem  20663  iblcnlem1  20692  reldv  20772  limciun  20796  dvexp  20854  dveflem  20878  lhop1lem  20912  lhop  20915  elply2  21130  elplyd  21136  ply1term  21138  ply0  21142  plymullem  21150  qaa  21255  pserulm  21353  pserdvlem2  21359  efcn  21374  sincosq1lem  21425  tangtx  21433  sincos4thpi  21441  sincos6thpi  21443  pige3  21445  efif1olem4  21467  logf1o  21482  relogf1o  21484  log1  21500  loge  21501  relogiso  21512  dvrelog  21548  relogcn  21549  logcn  21558  cxpcn3  21652  resqrcn  21653  leibpi  21803  log2ublem1  21807  birthday  21814  emcllem5  21859  harmonicbnd  21863  harmonicbnd2  21864  emgt0  21866  harmonicbnd3  21867  ppiltx  21981  ppiublem1  22007  ppiub  22009  bclbnd  22085  bpos1lem  22087  bposlem8  22096  lgsquadlem2  22160  2sqlem9  22178  2sqlem10  22179  chebbnd1  22187  selberg2lem  22265  pntrsumo1  22280  selbergsb  22290  pntpbnd  22303  uhgra0  22365  umgra0  22381  usgra0  22411  usgra1v  22430  cusgraexilem2  22497  cusgrasizeindslem2  22504  0wlk  22566  0trl  22567  wlkntrllem2  22581  wlkntrl  22583  0pth  22591  1pthonlem1  22610  usgrcyclnl2  22649  4cycl4dv  22675  vdgrf  22690  umgrabi  22726  vdegp1ai  22727  vdegp1bi  22728  konigsberg  22730  ex-dif  22752  ex-in  22754  ex-eprel  22762  ex-id  22763  ex-fl  22776  avril1  22778  2bornot2b  22779  grposn  22824  issubgoi  22919  0vfval  23106  vsfval  23135  ajmoi  23381  ajfuni  23382  normlem2  23635  norm3adifii  23672  hhip  23701  hlim0  23760  hlimcaui  23761  hlimf  23762  hhssnv  23787  shscli  23842  shsval2i  23912  h1de2i  24078  fh3i  24148  fh4i  24149  cm2mi  24151  qlaxr3i  24161  mayetes3i  24255  ho0f  24277  hoif  24280  hodidi  24313  ho0subi  24321  hosd1i  24348  adjmo  24358  nmopsetn0  24391  nmfnsetn0  24404  funadj  24412  funcnvadj  24419  nmcexi  24552  cnlnadjlem8  24600  nmoptri2i  24625  opsqrlem4  24669  hmopidmchi  24677  pjoci  24706  pjinvari  24717  abrexdomjm  25016  elim2ifim  25035  iundisj2f  25060  rinvf1o  25078  funcnvmptOLD  25116  dfcnv2  25124  snct  25141  dmct  25144  fpwrelmap  25163  iundisj2fi  25211  nn0srg  25371  rge0srg  25372  gsumle  25406  reofld  25487  rearchi  25489  xrge0slmod  25491  xrge0iifcnv  25542  xrge0pluscn  25549  recms  25568  zlmds  25573  zlmtset  25574  cnzh  25579  rezh  25580  qqhre  25626  esumfsup  25699  esumpcvgval  25707  hasheuni  25714  esumcvg  25715  dmsigagen  25767  measvuni  25808  voliune  25825  volfiniune  25826  ddemeas  25832  br2base  25864  dya2iocuni  25878  eulerpartlem1  25924  eulerpartlemt  25928  eulerpartgbij  25929  eulerpartlemgh  25935  coinfliprv  26015  ballotlem2  26021  ballotlemfc0  26025  ballotlemfcc  26026  ballotlemic  26039  ballotlem7  26068  ballotth  26070  plymul02  26098  signswmnd  26109  lgamgulm2  26168  lgamcvglem  26172  gamf  26175  subfacp1lem5  26218  subfacp1lem6  26219  kur14lem9  26248  cvmcov2  26310  cvmliftlem1  26320  cvmliftlem4  26323  cvmliftlem5  26324  ghomgrpilem2  26445  relexp0  26471  relexpsucr  26472  relexpsucl  26474  dfrtrclrec2  26485  rtrclreclem.refl  26486  rtrclreclem.subset  26487  rtrclreclem.min  26489  dfrtrcl2  26490  brtpid1  26517  brtpid2  26518  brtpid3  26519  fzp1nel  26549  fprodcom2  26647  faclimlem1  26701  domep  26759  axextndbi  26771  poseq  26867  wfrlem6  26882  wfrlem14  26890  wfrlem16  26892  frrlem10  26932  sltval2  26950  nosgnn0i  26953  brv  27061  txprel  27063  relsset  27072  relbigcup  27081  fvbigcup  27086  fnsingle  27103  fvsingle  27104  snelsingles  27106  funimage  27112  fullfunfnv  27130  imagesset  27137  ax5seglem7  27213  axlowdimlem4  27223  axlowdimlem6  27225  axlowdimlem7  27226  axlowdimlem10  27229  axlowdimlem13  27232  axlowdimlem16  27235  axlowdimlem17  27236  axlowdim  27239  funtransport  27304  colinrel  27330  funray  27413  funline  27415  bpolylem  27433  bpoly3  27443  bpoly4  27444  0hf  27457  waj-ax  27503  lukshef-ax2  27504  arg-ax  27505  limsucncmpi  27534  mblfinlem1  27608  mblfinlem2  27609  ismblfin  27612  voliunnfl  27615  cnambfre  27620  dvtanlem  27621  comppfsc  27759  neibastop2lem  27761  filnetlem3  27781  cover2  27787  abrexdom  27804  fdc  27821  cncfres  27846  heibor1lem  27890  bicontr  28062  tsim1  28084  moxfr  28172  mapfzcons1  28202  diophrw  28245  0dioph  28265  vdioph  28266  rabren3dioph  28302  2nn0ind  28434  rpnnen3  28529  kelac2lem  28565  frlmpwfi  28602  islinds2  28623  lhe4.4ex1a  28777  rusbcALT  28867  ipo0  28879  ifr0  28880  fnchoice  28926  stoweidlem13  28987  stoweidlem34  29008  stirlinglem5  29052  stirlinglem13  29060  stirlingr  29064  aistia  29090  aisfina  29091  aiffnbandciffatnotciffb  29097  axorbciffatcxorb  29098  abnotbtaxb  29109  abnotataxb  29110  usgra2pthspth  29476  usgra2pthlem1  29481  wwlknext  29537  wwlknfi  29551  disjxwwlkn  29745  frgra0  29767  numclwwlkdisj  29854  numclwwlk3lem  29882  ex-gte  29914  AnelBC  29949  empty-surprise  29986  eximp-surprise2  29989  vk15.4j  30079  2sb5nd  30115  dfvd1ir  30132  dfvd2anir  30144  dfvd2ir  30146  dfvd3ir  30153  dfvd3anir  30156  iden2  30183  e0bir  30357  uun2221p1  30394  uun2221p2  30395  2sb5ndVD  30492  2sb5ndALT  30514  iunconlem2  30517  bnj226  30571  bnj1101  30625  bnj110  30699  bnj149  30716  bnj150  30717  bnj151  30718  bnj517  30726  bnj580  30754  bnj865  30764  bnj900  30770  bnj996  30796  bnj1110  30821  bnj1133  30828  bnj1128  30829  bnj1145  30832  bnj1137  30834  bnj1171  30839  bnj1176  30844  bj-andnotimir  30914  bj-snsetex  30947  a6eNEW11  31022  sbtNEW11  31182  cbval2OLD11  31281  cbvex2OLD11  31282  nfsb4tw2AUXOLD11  31297  hlhilslem  34289
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 179
  Copyright terms: Public domain W3C validator