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

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

Proof of Theorem mpbi
StepHypRef Expression
1 mpbi.min . 2  |-  ph
2 mpbi.maj . . 3  |-  ( ph  <->  ps )
32biimpi 197 . 2  |-  ( ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187
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 188
This theorem is referenced by:  pm5.74i  248  notbii  297  pm5.19  361  ori  376  imori  414  pm4.71i  636  pm4.71ri  637  pm5.32i  641  pm3.24  890  pm5.16  898  biluk  941  4exmid  947  dn1  974  3ori  1324  trubifalOLD  1476  cadan  1505  nic-dfim  1546  nic-dfneg  1547  nic-mp  1548  nic-mpALT  1549  tbw-negdf  1576  rb-imdf  1627  mpgbi  1666  19.35i  1735  19.36iv  1814  19.37iv  1820  19.36i  2025  ax6  2062  sbie  2207  axi12  2400  bm1.1  2407  eqcomi  2431  eqtri  2444  eleqtri  2498  neii  2597  necomi  2649  neeqtri  2667  neli  2697  nrex  2813  rexlimi  2840  rexlimiv  2844  isseti  3022  vtocl2  3070  vtocl3  3071  eueq1  3179  euxfr2  3191  cdeqri  3221  sseqtri  3432  3sstr3i  3438  pssn2lp  3502  equncomi  3548  unssi  3577  ssini  3621  unabs  3639  inabs  3640  dfin4  3649  npss0  3769  difid  3801  disjdif  3805  difin0  3806  snid  3962  iinrab2  4298  symdifv  4313  rintn0  4329  breqtri  4383  axsep  4481  bm1.3ii  4485  ax6vsep  4486  zfnuleu  4487  notzfaus  4535  zfpow  4539  dtru  4551  reusv2lem4  4564  reuxfr2d  4580  dtruALT  4589  dtruALT2  4601  op1stb  4627  copsexg  4642  uniop  4659  pwundif  4696  relop  4940  rn0  5041  dmresi  5115  issref  5168  somincom  5189  cnvcnv  5243  rescnvcnv  5253  cnvcnvres  5254  cnvsn  5274  cocnvcnv2  5302  cores2  5303  co01  5305  relcoi1OLD  5320  cnviin  5328  onunisuci  5491  iota4an  5520  fnopab  5656  mpt0  5659  fnmpti  5660  f1cnvcnv  5740  f1ovi  5804  eliman0  5847  fvco4i  5896  fmpti  5997  fvsnun2  6052  funiunfv  6105  oprabss  6333  relmptopab  6468  zfun  6535  tfinds2  6641  omon  6654  2nd0  6751  f1stres  6766  f2ndres  6767  relmpt2opab  6826  df1st2  6830  df2nd2  6831  fsplit  6849  reldmtpos  6929  dftpos4  6940  tpostpos  6941  tpos0  6951  wfrlem4  6987  smo0  7025  tfrlem14  7057  tfrlem16  7059  rdgsucg  7089  rdglimg  7091  frfnom  7100  oawordeulem  7203  uniixp  7493  dfdom2  7542  ssdomg  7562  xpcomf1o  7607  sbthlem5  7632  pwdom  7670  limensuci  7694  fiint  7794  fidomdm  7799  pwfilem  7814  mptfi  7819  fisn  7887  dffi3  7891  ordtypelem6  7984  ordtypelem7  7985  wemaplem2  8008  wdompwdom  8039  harwdom  8051  suc11reg  8070  zfinf  8090  axinf2  8091  noinfep  8110  cantnfvalf  8115  cantnflt  8122  cantnf0  8125  cantnf  8143  tz9.1c  8159  tc2  8171  r111  8191  r1tr2  8193  r1ordg  8194  r1sssuc  8199  r1val1  8202  tz9.13  8207  r1elssi  8221  pwwf  8223  rankopb  8268  rankeq0b  8276  ranksuc  8281  rankmapu  8294  rankxplim  8295  rankxplim3  8297  rankxpsuc  8298  cp  8307  karden  8311  card0  8337  cardlim  8351  cardom  8365  infxpenlem  8389  alephsuc2  8455  alephgeom  8457  unialeph  8476  dfac4  8497  dfacacn  8515  cda1dif  8550  pm110.643  8551  infcda1  8567  ackbij1lem13  8606  ackbij2  8617  cf0  8625  cfsuc  8631  cfom  8638  cfslb2n  8642  ominf4  8686  fin23lem17  8712  fin23lem28  8714  fin23lem30  8716  fin23lem31  8717  fin23lem40  8725  isfin1-3  8760  dfacfin7  8773  fin1a2lem6  8779  itunitc1  8794  axcc3  8812  dcomex  8821  axdc2lem  8822  axcclem  8831  zfac  8834  ac3  8836  ackm  8839  axac2  8840  axac  8841  axaci  8842  cardeqv  8843  numth2  8845  numth  8846  brdom3  8900  fin71ac  8905  cardf  8919  aleph1  8940  cfpwsdom  8953  smobeth  8955  zfcndrep  8983  zfcndpow  8985  zfcndac  8988  gch2  9044  wunex3  9110  tskpr  9139  inar1  9144  rankcf  9146  tskcard  9150  tskuni  9152  grothpw  9195  axgroth4  9201  grothprim  9203  inaprc  9205  dmaddpi  9259  dmmulpi  9260  1lt2pi  9274  addpqf  9313  mulpqf  9315  1lt2nq  9342  supsrlem  9479  ssxr  9647  gtso  9659  subf  9821  negne0i  9893  negdiiOLD  9903  mulnzcnopr  10202  infrenegsup  10535  infmsupOLD  10536  halflt1  10775  nn0ssz  10902  zeo  10965  numlt  11014  numltc  11015  uzf  11106  uzinfmiOLD  11183  zgt1rpn0n1  11284  xaddf  11461  xsubge0  11491  xmulf  11502  infmxrclOLD  11546  infmxrlbOLD  11568  infmxrgelbOLD  11569  xrinfm0OLD  11571  ixxf  11589  ixxssxr  11591  iooval2  11613  ioof  11676  unirnioo  11678  dfioo2  11679  xrge0neqmnf  11681  fzval2  11731  fzf  11732  0nelfz1  11762  fz10  11764  fzpreddisj  11789  4fvwrd4  11853  fzof  11861  fzo0  11886  om2uzoi  12112  faclbnd4lem1  12421  hashkf  12460  hashgval  12461  hashinf  12463  hashresfn  12466  hashnn0n0nn  12513  hashbclem  12556  hashge3el3dif  12583  wrdexg  12623  rev0  12808  f1oun2prg  12939  trclublem  12996  sqrt2gt1lt2  13275  limsupgord  13464  limsupvalOLD  13468  fclim  13553  fsumrelem  13803  ackbijnn  13822  incexclem  13830  incexc  13831  arisum2  13855  georeclim  13864  geoisumr  13870  0.999...  13873  geoihalfsum  13874  risefall0lem  14015  ege2le3  14080  sin0  14139  ef01bndlem  14174  cos2bnd  14178  cos01gt0  14181  sincos2sgn  14184  sin4lt0  14185  rpnnen2lem3  14205  rpnnen2lem9  14211  rexpen  14216  cnso  14235  dvdslelem  14285  n2dvds1  14290  divalglem1  14308  divalglem5OLD  14312  divalglem5  14313  divalglem6  14314  divalglem10  14319  0bits  14349  sadcf  14363  sadcadd  14368  bitsshft  14385  smupf  14388  gcdf  14419  eucalgf  14478  2prm  14576  dfphi2  14658  pockthi  14787  prmreclem2  14797  prmrec  14802  vdwapf  14858  vdwap0  14862  vdwlem6  14872  ramvalOLD  14897  ramcl2lemOLD  14899  karatsuba  14992  1259lem5  15042  2503lem3  15046  4001lem4  15051  structcnvcnv  15068  structfn  15070  strlemor1  15153  strleun  15156  prdsval  15289  prdsds  15298  imasdsfnOLD  15363  imasdsvalOLD  15364  imasvscafn  15379  xpsc0  15402  xpsc1  15403  xpsff1o  15410  sscpwex  15656  wunfunc  15740  wunnat  15797  eldmcoa  15896  coapm  15902  catcfuccl  15940  catcxpccl  16028  yonedainv  16102  plusffval  16429  grpinvfvi  16643  mulgfvi  16698  symgsssg  17044  symgfisg  17045  psgnunilem5  17071  sylow3lem2  17216  oppglsm  17230  efgmf  17299  efgval  17303  efgsf  17315  0frgp  17365  gsumzaddlem  17490  dmdprd  17566  dprdval  17571  invrfval  17837  drngui  17917  scaffval  18045  lssintcl  18123  mplsubrglem  18599  opsrtoslem2  18644  cnfld0  18928  cnfld1  18929  cnfldsub  18932  xrsds  18947  psgnghm  19083  zrhpsgnmhm  19087  recrng  19124  ipffval  19150  ocv1  19177  dsmmbas2  19235  mdetralt  19568  maducoeval2  19600  eltpsi  19896  unitg  19917  fctop  19954  cctop  19956  ppttop  19957  epttop  19959  leordtvallem1  20161  leordtvallem2  20162  iccordt  20165  iscnp2  20190  discmp  20348  concompcld  20384  1stcrestlem  20402  2ndcdisj  20406  topnlly  20441  disllycmp  20448  dis1stc  20449  txuni2  20515  xkotf  20535  dfac14lem  20567  prdstps  20579  txindis  20584  tx1stc  20600  xkohaus  20603  xkoptsub  20604  cnmpt1st  20618  cnmpt2nd  20619  ptcmpfi  20763  filcon  20833  trfil1  20836  fin1aufil  20882  tgpconcompeqg  21061  tgpconcomp  21062  tsmsres  21093  trust  21179  met1stc  21471  dscmet  21522  nmovalOLD  21674  retopon  21719  cnfldtopon  21738  xrsxmet  21762  xrsmopn  21765  metdsvalOLD  21814  iimulcn  21901  icopnfhmeo  21906  iccpnfhmeo  21908  xrhmeo  21909  cnheiborlem  21917  lebnumii  21932  ishtpy  21938  htpycc  21946  pco1  21981  pcohtpylem  21985  pcopt  21988  pcopt2  21989  pcoass  21990  pcorevlem  21992  cfilresi  22200  rrxcph  22286  ovolvalOLD  22362  ovoliunlem3  22392  ovolicc1  22404  ovolicc2  22411  volf  22418  ioorf  22460  ioorfOLD  22465  dyadf  22484  dyadmbl  22493  vitalilem5  22505  vitali  22506  mbfimaopnlem  22546  mbflimsup  22558  mbflimsupOLD  22559  0plef  22565  i1fima  22571  i1fima2  22572  i1fd  22574  itg1ge0  22579  itg10  22581  i1f1lem  22582  i1fadd  22588  i1fmul  22589  i1fmulc  22596  mbfi1fseqlem5  22612  itg2addlem  22651  reldv  22760  dvbsss  22792  dvef  22867  lhop1lem  22900  deg1fvi  22969  plypf1  23101  coeeulem  23113  coeeu  23114  vieta1lem2  23199  aannenlem3  23221  aalioulem3  23225  dvradcnv  23311  pserulm  23312  pserdvlem2  23318  abelthlem6  23326  sinhalfpilem  23353  sincos4thpi  23403  tan4thpi  23404  sincos6thpi  23405  pige3  23407  resinf1o  23420  tanord1  23421  tanregt0  23423  efabl  23434  relogrn  23446  dfrelog  23450  logneg  23472  logltb  23484  logcn  23527  logf1o2  23530  dvlog  23531  efopnlem2  23537  efopn  23538  logccv  23543  dvsqrt  23617  dvcnsqrt  23619  cxpcn3  23623  logblog  23664  angpined  23691  1cubr  23703  asinsin  23753  asin1  23755  reasinsin  23757  atan0  23769  atanbnd  23787  atan1  23789  log2cnv  23805  log2ublem3  23809  log2ub  23810  log2le1  23811  birthday  23815  amgmlem  23850  emcllem5  23860  emgt0  23867  harmonicbnd3  23868  ftalem3  23934  basellem4  23945  sgmf  24007  ppi1  24026  cht1  24027  vma1  24028  ppiltx  24039  sqff1o  24044  ppiublem1  24065  ppiublem2  24066  ppiub  24067  chtub  24075  dchreq  24121  bposlem7  24153  bposlem8  24154  bposlem9  24155  lgsdir2lem2  24187  lgsdir2lem3  24188  chebbnd1  24245  chto1ub  24249  chpo1ubb  24254  pntibndlem1  24362  tgldimor  24481  tglnfn  24527  axlowdimlem4  24910  axlowdimlem16  24922  axlowdim  24926  umgrafi  24984  usgraexmplef  25063  usgraexmplc  25067  usgrafilem1  25074  2trllemA  25215  wlkntrllem1  25224  wlkntrllem3  25226  0pth  25235  spthispth  25238  2pthon  25267  2pthon3v  25269  constr3trllem3  25315  constr3pthlem3  25320  konigsberg  25650  frgrawopreg2  25714  ex-dif  25808  ex-un  25809  ex-in  25810  ex-fl  25832  avril1  25835  ginvsn  26012  cnid  26014  mulid  26019  rngosn3  26089  vcoprnelem  26132  vcex  26134  cnnvm  26249  ipasslem8  26413  ipasslem10  26415  hvsubf  26603  normlem1  26698  normlem6  26703  normlem7  26704  norm-ii-i  26725  norm3adifii  26736  hilid  26749  hlimf  26825  hhssabloi  26848  hhssnv  26850  hhshsslem1  26853  shincli  26950  shsval2i  26975  shs0i  27037  chj0i  27043  chm1i  27044  chincli  27048  chdmm1i  27065  shjshsi  27080  chsup0  27136  h1de2bi  27142  spansnpji  27166  cmcmlem  27179  cmcmii  27185  cmcm2ii  27186  cmcm3ii  27187  pjidmi  27261  pjssmii  27269  pj0i  27281  pjocini  27286  mayetes3i  27317  df0op2  27340  hoaddcomi  27360  hoaddassi  27364  hocadddiri  27367  hocsubdiri  27368  hoaddid1i  27374  ho0coi  27376  hoid1i  27377  hoid1ri  27378  hodseqi  27382  honegsubi  27384  adj1o  27482  hoddii  27577  lnopunilem1  27598  lnopunilem2  27599  nmcopexi  27615  nmcopex  27617  nmcoplb  27618  nmcfnexi  27639  nmcfnex  27641  nmcfnlb  27642  adjbd1o  27673  adjcoi  27688  nmopcoadji  27689  opsqrlem6  27733  pjsdii  27743  pjddii  27744  pjidmcoi  27765  pjtoi  27767  pjin1i  27780  pjclem1  27783  stji1i  27830  reuxfr3d  28060  inindif  28086  iuninc  28115  fnresin  28167  rinvf1o  28169  suppss2fOLD  28176  suppss2f  28177  xppreima  28187  ofoprabco  28206  funcnvmptOLD  28209  gtiso  28220  df1stres  28223  df2ndres  28224  snct  28238  dmct  28241  padct  28250  ffsrn  28257  fpwrelmapffs  28262  xrge0infssdOLD  28286  infxrge0lbOLD  28290  infxrge0glbOLD  28292  infxrge0gelbOLD  28294  nnindf  28326  nn0min  28328  ressplusf  28355  xrsclat  28386  xrge0base  28391  xrge00  28392  xrnarchi  28445  xrge0slmod  28552  locfinreflem  28612  locfinref  28613  unicls  28654  sqsscirc1  28659  mhmhmeotmd  28678  rmulccn  28679  raddcn  28680  xrge0iifiso  28686  xrge0iifhmeo  28687  lmxrge0  28703  cnzh  28719  rezh  28720  qqh0  28733  qqh1  28734  qqhre  28769  rrhre  28770  esumnul  28814  esum0  28815  esumsnf  28830  esumpfinvallem  28840  esumpfinvalf  28842  esumpcvgval  28844  esumcvgsum  28854  esumsup  28855  esumcvgre  28857  sigaclfu2  28888  dmsigagen  28911  ldgenpisyslem1  28930  ddemeas  29004  imambfm  29029  mbfmvolf  29033  br2base  29036  omsfvalOLD  29067  omsfOLD  29069  omssubadd  29073  oms0OLD  29074  omssubaddlemOLD  29076  omssubaddOLD  29077  carsgclctunlem3  29097  sibfof  29118  sitg0  29124  eulerpartlemt  29149  eulerpartgbij  29150  0rrv  29229  coinfliplem  29256  coinflipprob  29257  coinfliprv  29260  ballotlem2  29266  ballotlem4  29276  ballotlem5  29277  ballotlemi1  29280  ballotlem7  29313  ballotth  29315  ballotlemi1OLD  29318  ballotlem7OLD  29351  ballotthOLD  29353  signsplypnf  29384  signsply0  29385  signsw0g  29390  signswch  29395  signsvf0  29414  bnj521  29490  bnj1098  29540  bnj1109  29543  bnj1131  29544  bnj1533  29608  bnj151  29633  bnj580  29669  bnj852  29677  bnj864  29678  bnj865  29679  bnj978  29705  bnj1021  29720  bnj907  29721  bnj1093  29734  bnj1145  29747  bnj1172  29755  bnj1174  29757  bnj1176  29759  bnj1186  29761  subfacf  29843  subfacp1lem1  29847  subfacp1lem5  29852  subfacp1lem6  29853  subfacval3  29857  erdszelem2  29860  kur14lem4  29877  iooscon  29915  iccllyscon  29918  msrfo  30129  mthmpps  30165  problem5  30246  quad3  30247  ghomgrpilem1  30248  ghomgrpilem2  30249  circum  30263  axextprim  30273  axrepprim  30274  axunprim  30275  axinfprim  30278  axacprim  30279  inffz  30307  logi  30314  bcneg1  30316  setinds  30368  dfon2lem2  30374  dfon2lem4  30376  axextdfeq  30388  poseq  30435  frrlem4  30461  nosgnn0  30489  sltsolem1  30499  bdayfo  30506  fobigcup  30609  snelsingles  30631  fullfunfnv  30655  fullfunfv  30656  rankaltopb  30688  rank0  30879  rankeq1o  30880  hfuni  30893  fneer  30951  neibastop1  30957  nabi1i  30994  nabi2i  30995  limsucncmpi  31047  bj-consensusALT  31099  bj-nfxfr  31154  bj-axsep  31315  bj-zfpow  31317  bj-dtru  31319  bj-sbieOLD  31352  bj-sbidmOLD  31353  bj-n0i  31445  bj-snsetex  31462  bj-tagss  31479  bj-2upln0  31522  bj-2upln1upl  31523  bj-nuliota  31527  bj-elid  31540  bj-pinftyccb  31564  bj-minftyccb  31568  bj-pinftynminfty  31570  f1omptsnlem  31639  mptsnunlem  31641  topdifinffinlem  31651  relowlpssretop  31668  1oequni2o  31672  imadifss  31829  tan2h  31838  poimirlem3  31844  poimirlem9  31850  poimirlem16  31857  poimirlem17  31858  poimirlem18  31859  poimirlem19  31860  poimirlem20  31861  poimirlem22  31863  poimirlem30  31871  mblfinlem1  31878  mblfinlem2  31879  ovoliunnfl  31883  voliunnfl  31885  dvtanlemOLD  31892  itg2addnclem  31894  itg2addnclem2  31895  asindmre  31928  areacirclem1  31933  fdc  31975  cntotbnd  32029  heiborlem6  32049  rrnval  32060  reheibor  32072  prter2  32358  renegclALT  32441  mapdunirnN  35124  rntrclfvOAI  35439  diophrw  35507  rabren3dioph  35564  pellexlem6  35585  pellex  35586  frmx  35668  frmy  35669  jm2.23  35758  jm2.27dlem3  35773  axac10  35795  pw2f1ocnv  35799  kelac2lem  35829  lmhmlnmsplit  35852  pwfi2f1o  35861  frlmpwfi  35863  ifpbiidcor  36025  cnvnonrel  36101  rnnonrel  36104  resnonrel  36105  cononrel1  36107  cononrel2  36108  fvnonrel  36110  cnvcnvintabd  36113  cnvintabd  36116  rclexi  36129  rtrclex  36131  clcnvlem  36137  cnvrcl0  36139  dmtrcl  36141  rntrcl  36142  dfrtrcl5  36143  iunrelexp0  36201  dmtrclfvRP  36229  rntrclfv  36231  corcltrcl  36238  cotrclrcl  36241  0heALT  36286  frege54cor1a  36367  int-rightdistd  36534  int-sqdefd  36535  int-sqgeq0d  36540  seff  36564  expgrowthi  36589  expgrowth  36591  binomcxplemnotnn0  36612  ee233  36783  ax6e2nd  36832  in1  36849  dfvd2ani  36861  dfvd2i  36863  dfvd3i  36870  dfvd3ani  36873  e0bi  37073  uun2221  37110  uun2221p1  37111  uun2221p2  37112  en3lpVD  37151  relopabVD  37208  ax6e2ndVD  37215  ax6e2ndALT  37237  nnf1oxpnn  37370  negpilt0  37381  xrgtso  37459  ioontr  37497  iccdifioo  37502  iccdifprioo  37503  fsummulc1f  37525  fsumiunss  37532  icccncfext  37642  dvcosre  37658  dvsinax  37660  ioodvbdlimc1lem2  37681  ioodvbdlimc1lem2OLD  37683  ioodvbdlimc2lem  37685  ioodvbdlimc2lemOLD  37686  dvmptmulf  37689  dvnmul  37695  dvmptfprodlem  37696  dvnprodlem2  37699  stoweidlem1  37738  stoweidlem26  37763  stoweidlem34  37772  stoweidlem44  37782  stoweid  37802  stirlinglem5  37817  dirkercncflem1  37842  fourierdlem44  37892  fourierdlem56  37903  fourierdlem62  37909  fourierdlem89  37936  fourierdlem91  37938  fourierdlem100  37947  fourierdlem102  37949  fourierdlem103  37950  fourierdlem104  37951  fourierdlem108  37955  fourierdlem112  37959  fourierdlem114  37961  fouriersw  37972  gsumge0cl  38058  sge0tsms  38067  sge0ltfirpmpt2  38113  ovn0  38229  hoidmv1le  38257  hoidmvle  38263  axorbtnotaiffb  38298  axorbciffatcxorb  38300  abnotbtaxb  38311  1nevenALTV  38627  nnsum3primes4  38690  evengpoap3  38701  tgblthelfgott  38715  tgoldbachlt  38716  resisresindm  38812  residfi  38830  upgrfi  38951  ldepslinc  39889  3halfnz  39904  alimp-no-surprise  40107  aacllem  40127
  Copyright terms: Public domain W3C validator