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

Theorem mpbii 211
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbii.min  |-  ps
mpbii.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbii  |-  ( ph  ->  ch )

Proof of Theorem mpbii
StepHypRef Expression
1 mpbii.min . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpbii.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbid 210 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  elimh  956  ax12vOLD  1857  ax12v2  2084  ax12eq  2272  ax12el  2273  ax12inda  2279  ax12v2-o  2280  eqcomd  2465  eqvisset  3117  vtoclgf  3165  vtoclg1f  3166  eueq3  3274  sbc2or  3336  csbiegf  3454  un00  3865  elimhyp  4003  elimhyp2v  4004  elimhyp3v  4005  elimhyp4v  4006  elimdhyp  4008  keephyp2v  4010  keephyp3v  4011  sneqr  4199  preqr1  4206  preq12b  4208  prel12  4209  nfopd  4236  ssex  4600  pwne0  4626  opthwiener  4758  isso2i  4841  ordtri3or  4919  on0eqel  5004  nfimad  5356  dfrel2  5463  funsng  5640  cnvresid  5664  nffvd  5881  fnbrfvb  5913  fvelrnb  5920  fvelimab  5929  funfvop  6000  iunpw  6613  onsucuni  6662  onuninsuci  6674  tposf12  6998  oaword1  7219  oneo  7248  nnaword1  7296  nnneo  7318  inficl  7903  fipwuni  7904  infeq5i  8070  cantnflt  8108  cantnflem1  8125  cantnfltOLD  8138  cantnflem1OLD  8148  cnfcom  8161  cnfcomOLD  8169  rankidn  8257  rankr1id  8297  rankxpsuc  8317  iscard  8373  iscard2  8374  carduni  8379  cardmin2  8396  infxpenlem  8408  alephgeom  8480  cardaleph  8487  infenaleph  8489  iscard3  8491  alephsson  8498  alephfp  8506  alephval3  8508  dfac12k  8544  axdc3lem2  8848  alephval2  8964  alephreg  8974  cfpwsdom  8976  alephom  8977  axrepndlem1  8984  axunndlem1  8987  axunnd  8988  axpowndlem2  8990  axpowndlem2OLD  8991  axpowndlem3  8992  axpowndlem3OLD  8993  axpowndlem4  8994  axpownd  8995  axregndlem2  8997  axinfndlem1  9000  axinfnd  9001  axacndlem4  9005  axacndlem5  9006  axacnd  9007  gchaleph2  9067  elwina  9081  elina  9082  winaon  9083  inawina  9085  winainf  9089  winalim  9090  tskr1om2  9163  r1tskina  9177  gruina  9213  grur1a  9214  indpi  9302  nqerrel  9327  recidnq  9360  ltaddnq  9369  pncan3  9847  divcan2  10236  ltp1  10401  ltm1  10403  recreclt  10464  elnn0z  10898  nn0ind-raph  10985  fzdifsuc  11765  fsuppmapnn0fiubex  12101  faclbnd5  12379  hashfun  12499  2swrd2eqwrdeq  12903  caucvgrlem  13507  fsumcnv  13600  fprodcnv  13799  ef01bndlem  13931  sin01gt0  13937  cos01gt0  13938  egt2lt3  13951  cnso  13992  4sqlem12  14486  funcres  15312  fuchom  15377  xpsmnd  16087  mulgfval  16270  xpsgrp  16316  nmznsg  16372  symgplusg  16541  frgp0  16905  gsumval3OLD  17035  gsumval3lem1  17036  gsumval3lem2  17037  gsumval3  17038  pwssplit1  17832  mvrf1  18208  blssioo  21426  dvidlem  22445  dvcj  22479  dvrec  22484  rolle  22517  cmvth  22518  mvth  22519  dvlip  22520  dvlipcn  22521  dv11cn  22528  dvivthlem2  22536  lhop1lem  22540  lhop1  22541  lhop2  22542  q1peqb  22681  pserdv  22950  sinhalfpilem  22982  tangtx  23024  efabl  23063  logneg2  23126  lgseisenlem4  23753  dchrisum0lem3  23830  mulogsum  23843  pntrlog2bndlem1  23888  axlowdimlem7  24378  axlowdimlem10  24381  axcontlem6  24399  constr3lem2  24773  el2spthonot0  24998  frisusgranb  25124  extwwlkfablem2  25205  hsn0elch  26293  axpjcl  26445  omlsilem  26447  pjchi  26477  shs00i  26495  chj00i  26532  chabs1  26561  pjspansn  26622  chscllem1  26682  osumcor2i  26689  nonbooli  26696  atcvat4i  27443  xppreima  27635  xdivrec  27783  sqsscirc1  28051  1stmbfm  28404  2ndmbfm  28405  carsgclctunlem2  28461  eulerpartlemgh  28514  cvmlift3lem5  28965  cvmlift3lem7  28967  logi  29339  dfon2lem3  29434  dfon2lem7  29438  distel  29453  altopthsn  29816  dvasin  30308  areacirclem4  30315  heiborlem8  30519  0rngo  30629  islssfg2  31221  areaquad  31388  rnmptc  31652  fperdvper  31918  itgvol0  31970  stoweidlem13  31998  stoweidlem26  32011  stoweidlem34  32019  wallispilem4  32053  dirkercncflem1  32088  dirkercncflem3  32090  dirkercncflem4  32091  fourierdlem35  32127  fourierdlem73  32165  bnj1148  34195  bnj1154  34198  bj-elimhyp  34303  bj-axc15v  34473  bj-exlimmpbi  34621  lshpinN  34857  trlid0  36044  hdmap10lem  37712
  Copyright terms: Public domain W3C validator