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

Theorem mpbir 201
Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbir.min  |-  ps
mpbir.maj  |-  ( ph  <->  ps )
Assertion
Ref Expression
mpbir  |-  ph

Proof of Theorem mpbir
StepHypRef Expression
1 mpbir.min . 2  |-  ps
2 mpbir.maj . . 3  |-  ( ph  <->  ps )
32biimpri 198 . 2  |-  ( ps 
->  ph )
41, 3ax-mp 8 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  pm5.74ri  238  con4bii  289  orri  366  imorri  404  imnani  413  mpbir2an  887  mpbir3an  1136  tru  1327  nic-mpALT  1443  nic-ax  1444  nic-axALT  1445  mpto2OLD  1541  mtp-xor  1542  mtp-xorOLD  1543  mpgbir  1556  nfxfr  1576  19.35ri  1609  a9ev  1663  exiftruOLD  1665  exan  1892  ax12  1978  a9eOLD  1995  cbval2  2040  cbvex2  2041  sbt  2068  moaneu  2299  moanmo  2300  axi12  2369  axext2  2371  eqeltri  2459  nfcxfr  2522  neirr  2557  exmidne  2558  eqnetri  2569  mprgbir  2721  vex  2904  issetri  2908  moeq  3055  cdeqi  3091  ru  3105  eqsstri  3323  3sstr4i  3332  tpid1  3862  tpid2  3863  tpid3  3865  pwv  3958  uni0  3986  eqbrtri  4174  tr0  4256  trv  4257  zfrep4  4271  zfnuleu  4278  axnulALT  4279  0ex  4282  inex1  4287  0elpw  4312  axpow2  4322  axpow3  4323  pwex  4325  dvdemo1  4342  zfpair2  4347  exss  4369  moop2  4394  pwundif  4433  po0  4461  epse  4508  0elon  4577  nsuceq0  4604  uniex2  4646  snnex  4655  tfinds2  4785  finds  4813  finds2  4815  relsnop  4922  relxp  4925  rel0  4941  relopabi  4942  eliunxp  4954  opeliunxp2  4955  dmi  5026  xpidtr  5198  xpima  5255  cnvcnv  5265  dmsn0  5279  cnvsn0  5280  funmpt  5431  funmpt2  5432  isarep2  5475  fresaunres2  5557  f0  5569  f10  5651  f1o00  5652  f1oi  5655  f1osn  5657  brprcneu  5663  fvopab3ig  5744  opabex  5905  eufnfv  5913  mpt2fun  6113  reldmmpt2  6122  oprabex  6128  oprabex3  6129  ovid  6131  ovidig  6132  ovidi  6133  ovig  6136  ov3  6151  caovmo  6225  relmptopab  6233  f1stres  6309  f2ndres  6310  relmpt2opab  6370  tpos0  6447  porpss  6464  opabiotafun  6474  canth  6477  ncanth  6478  issmo  6548  tfrlem6  6581  tfrlem8  6583  tfrlem16  6592  tfr1a  6593  tfr1  6596  tz7.44lem1  6601  seqomlem2  6646  seqomlem3  6647  seqomlem4  6648  fnseqom  6650  abianfp  6654  0lt1o  6686  0we1  6688  eqer  6876  ecopover  6946  th3qcor  6950  mapsnf1o3  7000  ssdomg  7091  ensn1  7109  snfi  7125  xpcomf1o  7135  map2xp  7215  limensuci  7221  sdom1  7246  unblem4  7300  fidomdm  7326  marypha1lem  7375  hartogslem1  7446  hartogs  7448  card2on  7457  ruv  7503  ruALT  7504  inf2  7513  inf3lem6  7523  infeq5i  7526  zfinf2  7532  cantnflt  7562  cantnf  7584  mapfien  7588  cnfcom  7592  trcl  7599  tz9.1c  7601  tc2  7616  r1funlim  7627  r1fnon  7628  karden  7754  tskwe  7772  cardprclem  7801  cardprc  7802  pm54.43  7822  r0weon  7829  iunmapdisj  7839  alephfnon  7881  alephfplem4  7923  alephfp  7924  alephval3  7926  aceq3lem  7936  kmlem2  7966  cda1dif  7991  ackbij1  8053  ackbij2lem2  8055  ackbij2  8058  infpssrlem3  8120  hsmexlem4  8244  hsmexlem5  8245  axdc3lem4  8268  ac2  8276  axac3  8279  ac6  8295  axdclem2  8335  ondomon  8373  alephsucpw  8380  pwcfsdom  8393  cfpwsdom  8394  smobeth  8396  axpowndlem3  8409  zfcndun  8425  zfcndpow  8426  zfcndinf  8428  zfcndac  8429  wunex2  8548  uniwun  8550  wuncval2  8557  grur1  8630  axgroth5  8634  axgroth2  8635  axgroth6  8638  axgroth3  8641  grothtsk  8645  inaprc  8646  ltsopi  8700  dmaddpi  8702  dmmulpi  8703  1lt2pi  8717  nqerf  8742  addnqf  8760  mulnqf  8761  1lt2nq  8785  m1p1sr  8902  m1m1sr  8903  0lt1sr  8905  axaddf  8955  axmulf  8956  ax1cn  8959  ax1ne0  8970  pnfnre  9062  mnfnre  9063  subaddrii  9323  ine0  9403  ixi  9585  recgt0ii  9850  nn1suc  9955  4d2e2  10066  nnunb  10151  arch  10152  un0mulcl  10188  nummac  10348  uzf  10425  indstr  10479  mnfltpnf  10657  ixxf  10860  ioof  10936  fzf  10981  fzp1disj  11038  fzof  11069  om2uzrani  11221  om2uzf1oi  11222  uzrdglem  11226  uzrdgfni  11227  uzrdg0i  11228  ltwenn  11231  hashgf1o  11239  axdc4uzlem  11250  sq0  11402  irec  11409  hashkf  11549  hashf  11554  hash0  11575  hashsslei  11614  hashxplem  11625  hashbclem  11630  hashf1lem1  11633  wrd0  11661  wrdexg  11668  revs1  11726  cats1fvn  11751  climmo  12280  fsumcom2  12487  ackbijnn  12536  incexclem  12545  infcvgaux1i  12565  efcvgfsum  12617  cos1bnd  12717  cos2bnd  12718  eirr  12733  znnen  12741  qnnen  12742  aleph1re  12773  sqr2irr  12777  nthruz  12780  dvdslelem  12823  3dvds  12841  divalglem5  12846  bitsf  12868  sadcaddlem  12898  sadadd2lem  12900  sadadd3  12902  sadaddlem  12907  isprm3  13017  2prm  13024  phicl2  13086  pockthi  13204  unbenlem  13205  prmrec  13219  vdwlem13  13290  vdwnn  13295  ramcl2  13313  mod2xnegi  13336  modsubi  13337  structcnvcnv  13409  structfun  13410  setsres  13424  strfv  13430  strlemor1  13485  strleun  13488  0rest  13586  firest  13589  restid  13590  prdsval  13607  prdsbas  13609  prdsplusg  13610  prdsmulr  13611  prdsvsca  13612  prdsds  13615  imasaddfnlem  13682  imasvscafn  13691  oppchomfval  13869  oppcbas  13873  2oppchomf  13879  rescbas  13958  rescco  13961  rescabs  13962  idfucl  14007  wunnat  14082  homarel  14120  dmaf  14133  cdaf  14134  catcfuccl  14193  relxpchom  14207  catcxpccl  14233  oppchofcl  14286  oyoncl  14296  odubas  14489  letsr  14601  mgmidmo  14622  releqg  14916  ga0  15004  oppglem  15075  efgval  15278  efger  15279  efgsp1  15298  efgsfo  15300  efgredleme  15304  efgredlem  15308  efgred  15309  cygctb  15430  gsum2d2lem  15476  gsum2d2  15477  gsumcom2  15478  dprd2d2  15531  pgpfaclem1  15568  mgplem  15582  mgpress  15588  opprlem  15662  reldvdsr  15678  00lsp  15986  sralem  16178  srasca  16182  psrvscafval  16383  opsrbaslem  16467  psrbag0  16483  00ply1bas  16563  ply1plusgfvi  16565  zlmsca  16727  znbaslem  16744  ocvfval  16818  ocv0  16829  cssval  16834  thlbas  16848  thlle  16849  eltopspOLD  16908  tgdom  16968  tgidm  16970  indistps2ALT  17003  restbas  17146  resttopon  17149  rest0  17157  leordtval2  17200  iocpnfordt  17203  icomnfordt  17204  iooordt  17205  cnpfval  17222  iscnp2  17227  ist1-3  17337  1stcfb  17431  islly2  17470  1stckgen  17509  ptbasfi  17536  xkotf  17540  dfac14  17573  opnfbas  17797  zfbas  17851  hauspwpwf1  17942  alexsubALTlem4  18004  alexsubALT  18005  ptcmplem5  18010  cnextrel  18017  ust0  18172  tuslem  18220  0met  18306  prdsdsf  18307  prdsxmetlem  18308  prdsmet  18310  setsmsbas  18397  setsmsds  18398  prdsbl  18413  tngds  18562  qtopbaslem  18665  xrtgioo  18710  xrsdsre  18714  zcld  18717  recld2  18718  sszcld  18721  reperflem  18722  retopcon  18733  iccpnfcnv  18842  bndth  18856  ishtpy  18870  nmoleub2lem2  18997  recmet  19147  resscdrg  19181  ishl2  19193  volf  19294  iundisj2  19312  volsup  19319  icombl  19327  ioombl  19328  ismbf3d  19415  0plef  19433  0pledm  19434  itg1ge0  19447  mbfi1fseqlem5  19480  itg2addlem  19519  iblcnlem1  19548  reldv  19626  limciun  19650  dvexp  19708  dveflem  19732  lhop1lem  19766  lhop  19769  elply2  19984  elplyd  19990  ply1term  19992  ply0  19996  plymullem  20004  qaa  20109  aaliou3  20137  pserulm  20207  pserdvlem2  20213  efcn  20228  sincosq1lem  20274  tangtx  20282  sincos4thpi  20290  sincos6thpi  20292  pige3  20294  efif1olem4  20316  logf1o  20331  relogf1o  20333  log1  20349  loge  20350  relogiso  20361  dvrelog  20397  relogcn  20398  logcn  20407  cxpcn3  20501  resqrcn  20502  leibpi  20651  log2ublem1  20655  birthday  20662  emcllem5  20707  harmonicbnd  20711  harmonicbnd2  20712  emgt0  20714  harmonicbnd3  20715  ppiltx  20829  ppiublem1  20855  ppiub  20857  bclbnd  20933  bpos1lem  20935  bposlem8  20944  lgsquadlem2  21008  2sqlem9  21026  2sqlem10  21027  chebbnd1  21035  selberg2lem  21113  pntrsumo1  21128  selbergsb  21138  pntpbnd  21151  uhgra0  21213  umgra0  21229  usgra0  21259  usgra1v  21277  cusgraexilem2  21344  cusgrasizeindslem2  21351  0wlk  21411  0trl  21412  wlkntrllem2  21416  wlkntrllem3  21417  wlkntrllem4  21418  0pth  21426  1pthonlem1  21439  usgrcyclnl2  21478  4cycl4dv  21504  vdgrf  21519  umgrabi  21555  vdegp1ai  21556  vdegp1bi  21557  konigsberg  21559  ex-dif  21581  ex-in  21583  ex-eprel  21591  ex-id  21592  ex-fl  21605  avril1  21607  2bornot2b  21608  grposn  21653  issubgoi  21748  0vfval  21935  vsfval  21964  ajmoi  22210  ajfuni  22211  normlem2  22463  norm3adifii  22500  hhip  22529  hlim0  22588  hlimcaui  22589  hlimf  22590  hhssnv  22614  shscli  22669  shsval2i  22739  h1de2i  22905  fh3i  22975  fh4i  22976  cm2mi  22978  qlaxr3i  22988  mayetes3i  23082  ho0f  23104  hoif  23107  hodidi  23140  ho0subi  23148  hosd1i  23175  adjmo  23185  nmopsetn0  23218  nmfnsetn0  23231  funadj  23239  funcnvadj  23246  nmcexi  23379  cnlnadjlem8  23427  nmoptri2i  23452  opsqrlem4  23496  hmopidmchi  23504  pjoci  23533  pjinvari  23544  abrexdomjm  23834  elim2ifim  23852  iundisj2f  23875  rinvf1o  23887  funcnvmptOLD  23925  snct  23946  dmct  23949  iundisj2fi  23993  xrge0iifcnv  24125  xrge0pluscn  24132  recms  24147  zlmds  24151  zlmtset  24152  qqhre  24184  rrhre  24185  esumfsup  24258  esumpcvgval  24266  hasheuni  24273  esumcvg  24274  dmsigagen  24325  measvuni  24364  voliune  24381  volfiniune  24382  br2base  24415  dya2iocuni  24429  coinfliprv  24521  ballotlem2  24527  ballotlemfc0  24531  ballotlemfcc  24532  ballotlemic  24545  ballotlem7  24574  ballotth  24576  lgamgulm2  24601  lgamcvglem  24605  gamf  24608  subfacp1lem5  24651  subfacp1lem6  24652  kur14lem9  24681  cvmcov2  24743  cvmliftlem1  24753  cvmliftlem4  24756  cvmliftlem5  24757  ghomgrpilem2  24878  relexp0  24910  relexpsucr  24911  relexpsucl  24913  dfrtrclrec2  24924  rtrclreclem.refl  24925  rtrclreclem.subset  24926  rtrclreclem.min  24928  dfrtrcl2  24929  brtpid1  24959  brtpid2  24960  brtpid3  24961  fzp1nel  24991  faclimlem1  25122  domep  25175  axextndbi  25187  poseq  25279  wfrlem14  25295  wfrlem16  25297  frrlem10  25318  sltval2  25336  nosgnn0i  25339  brv  25443  txprel  25445  relsset  25454  relbigcup  25463  fvbigcup  25468  fnsingle  25484  fvsingle  25485  snelsingles  25487  funimage  25493  fullfunfnv  25511  ax5seglem7  25590  axlowdimlem4  25600  axlowdimlem6  25602  axlowdimlem7  25603  axlowdimlem10  25606  axlowdimlem13  25609  axlowdimlem16  25612  axlowdimlem17  25613  axlowdim  25616  funtransport  25681  colinrel  25707  funray  25790  funline  25792  bpolylem  25810  bpoly3  25820  bpoly4  25821  0hf  25834  waj-ax  25880  lukshef-ax2  25881  arg-ax  25882  limsucncmpi  25911  voliunnfl  25957  itgaddnclem2  25966  comppfsc  26080  neibastop2lem  26082  filnetlem3  26102  cover2  26108  abrexdom  26125  fdc  26142  cncfres  26167  heibor1lem  26211  moxfr  26426  mapfzcons1  26466  diophrw  26510  0dioph  26530  vdioph  26531  rabren3dioph  26569  2nn0ind  26701  rpnnen3  26796  kelac2lem  26833  frlmpwfi  26933  islinds2  26954  psgnunilem3  27090  psgnunilem4  27091  matsca  27141  lhe4.4ex1a  27217  rusbcALT  27310  ipo0  27322  ifr0  27323  fnchoice  27370  stoweidlem13  27432  stoweidlem34  27453  stirlinglem5  27497  stirlinglem13  27505  stirlingr  27509  aistia  27535  aisfina  27536  aiffnbandciffatnotciffb  27542  axorbciffatcxorb  27543  abnotbtaxb  27554  abnotataxb  27555  frgra0  27749  ex-gte  27820  AnelBC  27855  vk15.4j  27957  2sb5nd  27992  dfvd1ir  28007  dfvd2anir  28019  dfvd2ir  28021  dfvd3ir  28028  dfvd3anir  28031  iden2  28058  e0bir  28232  uun2221p1  28269  uun2221p2  28270  2sb5ndVD  28365  2sb5ndALT  28388  bnj226  28441  bnj1101  28495  bnj110  28569  bnj149  28586  bnj150  28587  bnj151  28588  bnj517  28596  bnj580  28624  bnj865  28634  bnj900  28640  bnj996  28666  bnj1110  28691  bnj1133  28698  bnj1128  28699  bnj1145  28702  bnj1137  28704  bnj1171  28709  bnj1176  28714  a9eNEW7  28810  sbtNEW7  28966  cbval2OLD7  29048  cbvex2OLD7  29049  nfsb4tw2AUXOLD7  29064  hlhilslem  32058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator