MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir Structured version   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  1330  nic-mpALT  1446  nic-ax  1447  nic-axALT  1448  mpto2OLD  1544  mtp-xor  1545  mtp-xorOLD  1546  mpgbir  1559  nfxfr  1579  19.35ri  1612  a9ev  1668  exiftruOLD  1670  exan  1903  cbval2OLD  1990  cbvex2  1991  ax12  2019  a9eOLD  2034  sbt  2126  sbie  2149  moaneu  2340  moanmo  2341  axi12  2415  axext2  2418  eqeltri  2506  nfcxfr  2569  neir  2604  neirr  2606  exmidne  2607  eqnetri  2618  nesymir  2642  nelir  2698  mprgbir  2776  vex  2959  issetri  2963  moeq  3110  cdeqi  3146  eqsstri  3378  3sstr4i  3387  tpid1  3917  tpid2  3918  tpid3  3920  pwv  4014  uni0  4042  eqbrtri  4231  tr0  4313  trv  4314  zfrep4  4328  zfnuleu  4335  axnulALT  4336  0ex  4339  inex1  4344  0elpw  4369  axpow2  4379  axpow3  4380  pwex  4382  dvdemo1  4399  zfpair2  4404  exss  4426  moop2  4451  pwundif  4490  po0  4518  epse  4565  0elon  4634  uniex2  4704  snnex  4713  tfinds2  4843  finds  4871  finds2  4873  relsnop  4980  relxp  4983  rel0  4999  relopabi  5000  eliunxp  5012  opeliunxp2  5013  dmi  5084  xpidtr  5256  xpima  5313  cnvcnv  5323  dmsn0  5337  cnvsn0  5338  funmpt  5489  funmpt2  5490  isarep2  5533  fresaunres2  5615  f0  5627  f10  5709  f1o00  5710  f1oi  5713  f1osn  5715  brprcneu  5721  fvopab3ig  5803  opabex  5964  eufnfv  5972  mpt2fun  6172  reldmmpt2  6181  oprabex  6187  oprabex3  6188  ovid  6190  ovidig  6191  ovidi  6192  ovig  6195  ov3  6210  caovmo  6284  relmptopab  6292  f1stres  6368  f2ndres  6369  relmpt2opab  6429  tpos0  6509  porpss  6526  opabiotafun  6536  canth  6539  ncanth  6540  issmo  6610  tfrlem6  6643  tfrlem8  6645  tfrlem16  6654  tfr1a  6655  tfr1  6658  tz7.44lem1  6663  seqomlem2  6708  seqomlem3  6709  seqomlem4  6710  fnseqom  6712  abianfp  6716  0lt1o  6748  0we1  6750  eqer  6938  ecopover  7008  th3qcor  7012  mapsnf1o3  7062  ssdomg  7153  ensn1  7171  snfi  7187  xpcomf1o  7197  map2xp  7277  limensuci  7283  sdom1  7308  unblem4  7362  fidomdm  7388  marypha1lem  7438  hartogslem1  7511  hartogs  7513  card2on  7522  ruALT  7569  inf2  7578  inf3lem6  7588  infeq5i  7591  zfinf2  7597  cantnflt  7627  cantnf  7649  mapfien  7653  cnfcom  7657  trcl  7664  tz9.1c  7666  tc2  7681  r1funlim  7692  r1fnon  7693  karden  7819  tskwe  7837  cardprclem  7866  pm54.43  7887  r0weon  7894  iunmapdisj  7904  alephfnon  7946  alephfplem4  7988  alephfp  7989  alephval3  7991  aceq3lem  8001  kmlem2  8031  cda1dif  8056  ackbij1  8118  ackbij2lem2  8120  ackbij2  8123  infpssrlem3  8185  hsmexlem4  8309  hsmexlem5  8310  axdc3lem4  8333  ac2  8341  axac3  8344  ac6  8360  axdclem2  8400  ondomon  8438  alephsucpw  8445  pwcfsdom  8458  cfpwsdom  8459  smobeth  8461  axpowndlem3  8474  zfcndun  8490  zfcndpow  8491  zfcndinf  8493  zfcndac  8494  wunex2  8613  uniwun  8615  wuncval2  8622  grur1  8695  axgroth5  8699  axgroth2  8700  axgroth6  8703  axgroth3  8706  grothtsk  8710  inaprc  8711  ltsopi  8765  dmaddpi  8767  dmmulpi  8768  1lt2pi  8782  nqerf  8807  addnqf  8825  mulnqf  8826  1lt2nq  8850  m1p1sr  8967  m1m1sr  8968  0lt1sr  8970  axaddf  9020  axmulf  9021  ax1cn  9024  subaddrii  9389  ixi  9651  recgt0ii  9916  nn1suc  10021  4d2e2  10132  arch  10218  un0mulcl  10254  nummac  10414  uzf  10491  indstr  10545  mnfltpnf  10723  ixxf  10926  ioof  11002  fzf  11047  fzp1disj  11105  fzof  11137  om2uzrani  11292  om2uzf1oi  11293  uzrdglem  11297  uzrdgfni  11298  uzrdg0i  11299  ltwenn  11302  hashgf1o  11310  axdc4uzlem  11321  sq0  11473  irec  11480  hashkf  11620  hashf  11625  hash0  11646  hashsslei  11685  hashxplem  11696  hashbclem  11701  hashf1lem1  11704  wrd0  11732  wrdexg  11739  revs1  11797  cats1fvn  11822  climmo  12351  fsumcom2  12558  ackbijnn  12607  incexclem  12616  infcvgaux1i  12636  efcvgfsum  12688  cos1bnd  12788  cos2bnd  12789  znnen  12812  qnnen  12813  aleph1re  12844  nthruz  12851  dvdslelem  12894  3dvds  12912  divalglem5  12917  bitsf  12939  sadcaddlem  12969  sadadd2lem  12971  sadadd3  12973  sadaddlem  12978  isprm3  13088  2prm  13095  phicl2  13157  pockthi  13275  unbenlem  13276  prmrec  13290  vdwlem13  13361  vdwnn  13366  ramcl2  13384  mod2xnegi  13407  modsubi  13408  structcnvcnv  13480  structfun  13481  setsres  13495  strfv  13501  strlemor1  13556  strleun  13559  0rest  13657  firest  13660  restid  13661  prdsval  13678  prdsbas  13680  prdsplusg  13681  prdsmulr  13682  prdsvsca  13683  prdsds  13686  imasaddfnlem  13753  imasvscafn  13762  oppchomfval  13940  oppcbas  13944  2oppchomf  13950  rescbas  14029  rescco  14032  rescabs  14033  idfucl  14078  wunnat  14153  homarel  14191  dmaf  14204  cdaf  14205  catcfuccl  14264  relxpchom  14278  catcxpccl  14304  oppchofcl  14357  oyoncl  14367  odubas  14560  letsr  14672  mgmidmo  14693  releqg  14987  ga0  15075  oppglem  15146  efgval  15349  efger  15350  efgsp1  15369  efgsfo  15371  efgredleme  15375  efgredlem  15379  efgred  15380  cygctb  15501  gsum2d2lem  15547  gsum2d2  15548  gsumcom2  15549  dprd2d2  15602  pgpfaclem1  15639  mgplem  15653  mgpress  15659  opprlem  15733  reldvdsr  15749  00lsp  16057  sralem  16249  srasca  16253  psrvscafval  16454  opsrbaslem  16538  psrbag0  16554  00ply1bas  16634  ply1plusgfvi  16636  zlmsca  16802  znbaslem  16819  ocvfval  16893  ocv0  16904  cssval  16909  thlbas  16923  thlle  16924  eltopspOLD  16983  tgdom  17043  tgidm  17045  indistps2ALT  17078  restbas  17222  resttopon  17225  rest0  17233  leordtval2  17276  iocpnfordt  17279  icomnfordt  17280  iooordt  17281  cnpfval  17298  iscnp2  17303  ist1-3  17413  1stcfb  17508  islly2  17547  1stckgen  17586  ptbasfi  17613  xkotf  17617  dfac14  17650  opnfbas  17874  hauspwpwf1  18019  alexsubALTlem4  18081  alexsubALT  18082  ptcmplem5  18087  cnextrel  18094  ust0  18249  tuslem  18297  0met  18396  prdsdsf  18397  prdsxmetlem  18398  prdsmet  18400  setsmsbas  18505  setsmsds  18506  prdsbl  18521  tngds  18689  qtopbaslem  18792  xrtgioo  18837  xrsdsre  18841  zcld  18844  recld2  18845  sszcld  18848  reperflem  18849  retopcon  18860  iccpnfcnv  18969  bndth  18983  ishtpy  18997  nmoleub2lem2  19124  recmet  19276  resscdrg  19312  ishl2  19324  volf  19425  iundisj2  19443  volsup  19450  icombl  19458  ioombl  19459  ismbf3d  19546  0plef  19564  0pledm  19565  itg1ge0  19578  mbfi1fseqlem5  19611  itg2addlem  19650  iblcnlem1  19679  reldv  19757  limciun  19781  dvexp  19839  dveflem  19863  lhop1lem  19897  lhop  19900  elply2  20115  elplyd  20121  ply1term  20123  ply0  20127  plymullem  20135  qaa  20240  pserulm  20338  pserdvlem2  20344  efcn  20359  sincosq1lem  20405  tangtx  20413  sincos4thpi  20421  sincos6thpi  20423  pige3  20425  efif1olem4  20447  logf1o  20462  relogf1o  20464  log1  20480  loge  20481  relogiso  20492  dvrelog  20528  relogcn  20529  logcn  20538  cxpcn3  20632  resqrcn  20633  leibpi  20782  log2ublem1  20786  birthday  20793  emcllem5  20838  harmonicbnd  20842  harmonicbnd2  20843  emgt0  20845  harmonicbnd3  20846  ppiltx  20960  ppiublem1  20986  ppiub  20988  bclbnd  21064  bpos1lem  21066  bposlem8  21075  lgsquadlem2  21139  2sqlem9  21157  2sqlem10  21158  chebbnd1  21166  selberg2lem  21244  pntrsumo1  21259  selbergsb  21269  pntpbnd  21282  uhgra0  21344  umgra0  21360  usgra0  21390  usgra1v  21409  cusgraexilem2  21476  cusgrasizeindslem2  21483  0wlk  21545  0trl  21546  wlkntrllem2  21560  wlkntrl  21562  0pth  21570  1pthonlem1  21589  usgrcyclnl2  21628  4cycl4dv  21654  vdgrf  21669  umgrabi  21705  vdegp1ai  21706  vdegp1bi  21707  konigsberg  21709  ex-dif  21731  ex-in  21733  ex-eprel  21741  ex-id  21742  ex-fl  21755  avril1  21757  2bornot2b  21758  grposn  21803  issubgoi  21898  0vfval  22085  vsfval  22114  ajmoi  22360  ajfuni  22361  normlem2  22613  norm3adifii  22650  hhip  22679  hlim0  22738  hlimcaui  22739  hlimf  22740  hhssnv  22764  shscli  22819  shsval2i  22889  h1de2i  23055  fh3i  23125  fh4i  23126  cm2mi  23128  qlaxr3i  23138  mayetes3i  23232  ho0f  23254  hoif  23257  hodidi  23290  ho0subi  23298  hosd1i  23325  adjmo  23335  nmopsetn0  23368  nmfnsetn0  23381  funadj  23389  funcnvadj  23396  nmcexi  23529  cnlnadjlem8  23577  nmoptri2i  23602  opsqrlem4  23646  hmopidmchi  23654  pjoci  23683  pjinvari  23694  abrexdomjm  23988  elim2ifim  24006  iundisj2f  24030  rinvf1o  24042  funcnvmptOLD  24082  snct  24103  dmct  24106  iundisj2fi  24153  xrge0iifcnv  24319  xrge0pluscn  24326  recms  24343  zlmds  24348  zlmtset  24349  cnzh  24354  rezh  24355  qqhre  24386  esumfsup  24460  esumpcvgval  24468  hasheuni  24475  esumcvg  24476  dmsigagen  24527  measvuni  24568  voliune  24585  volfiniune  24586  br2base  24619  dya2iocuni  24633  coinfliprv  24740  ballotlem2  24746  ballotlemfc0  24750  ballotlemfcc  24751  ballotlemic  24764  ballotlem7  24793  ballotth  24795  lgamgulm2  24820  lgamcvglem  24824  gamf  24827  subfacp1lem5  24870  subfacp1lem6  24871  kur14lem9  24900  cvmcov2  24962  cvmliftlem1  24972  cvmliftlem4  24975  cvmliftlem5  24976  ghomgrpilem2  25097  relexp0  25129  relexpsucr  25130  relexpsucl  25132  dfrtrclrec2  25143  rtrclreclem.refl  25144  rtrclreclem.subset  25145  rtrclreclem.min  25147  dfrtrcl2  25148  brtpid1  25178  brtpid2  25179  brtpid3  25180  fzp1nel  25210  fprodcom2  25308  faclimlem1  25362  domep  25420  axextndbi  25432  poseq  25528  wfrlem6  25543  wfrlem14  25551  wfrlem16  25553  frrlem10  25593  sltval2  25611  nosgnn0i  25614  brv  25722  txprel  25724  relsset  25733  relbigcup  25742  fvbigcup  25747  fnsingle  25764  fvsingle  25765  snelsingles  25767  funimage  25773  fullfunfnv  25791  imagesset  25798  ax5seglem7  25874  axlowdimlem4  25884  axlowdimlem6  25886  axlowdimlem7  25887  axlowdimlem10  25890  axlowdimlem13  25893  axlowdimlem16  25896  axlowdimlem17  25897  axlowdim  25900  funtransport  25965  colinrel  25991  funray  26074  funline  26076  bpolylem  26094  bpoly3  26104  bpoly4  26105  0hf  26118  waj-ax  26164  lukshef-ax2  26165  arg-ax  26166  limsucncmpi  26195  mblfinlem1  26243  mblfinlem2  26244  ismblfin  26247  voliunnfl  26250  cnambfre  26255  comppfsc  26387  neibastop2lem  26389  filnetlem3  26409  cover2  26415  abrexdom  26432  fdc  26449  cncfres  26474  heibor1lem  26518  moxfr  26733  mapfzcons1  26773  diophrw  26817  0dioph  26837  vdioph  26838  rabren3dioph  26876  2nn0ind  27008  rpnnen3  27103  kelac2lem  27139  frlmpwfi  27239  islinds2  27260  psgnunilem3  27396  psgnunilem4  27397  matsca  27447  lhe4.4ex1a  27523  rusbcALT  27616  ipo0  27628  ifr0  27629  fnchoice  27676  stoweidlem13  27738  stoweidlem34  27759  stirlinglem5  27803  stirlinglem13  27811  stirlingr  27815  aistia  27841  aisfina  27842  aiffnbandciffatnotciffb  27848  axorbciffatcxorb  27849  abnotbtaxb  27860  abnotataxb  27861  cshw1  28275  usgra2pthspth  28305  usgra2pthlem1  28310  frgra0  28384  ex-gte  28472  AnelBC  28507  vk15.4j  28612  2sb5nd  28647  dfvd1ir  28664  dfvd2anir  28676  dfvd2ir  28678  dfvd3ir  28685  dfvd3anir  28688  iden2  28715  e0bir  28889  uun2221p1  28926  uun2221p2  28927  2sb5ndVD  29022  2sb5ndALT  29044  iunconlem2  29047  bnj226  29101  bnj1101  29155  bnj110  29229  bnj149  29246  bnj150  29247  bnj151  29248  bnj517  29256  bnj580  29284  bnj865  29294  bnj900  29300  bnj996  29326  bnj1110  29351  bnj1133  29358  bnj1128  29359  bnj1145  29362  bnj1137  29364  bnj1171  29369  bnj1176  29374  a9eNEW7  29470  sbtNEW7  29631  cbval2OLD7  29730  cbvex2OLD7  29731  nfsb4tw2AUXOLD7  29746  hlhilslem  32739
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