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, 5-Aug-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  942  ax12v2  2034  ax12vALT  2135  ax12eq  2245  ax12el  2246  ax12inda  2252  ax12v2-o  2253  eqvisset  2972  vtoclgf  3019  vtoclg1f  3020  eueq3  3125  sbc2or  3185  csbiegf  3302  un00  3704  elimhyp  3838  elimhyp2v  3839  elimhyp3v  3840  elimhyp4v  3841  elimdhyp  3843  keephyp2v  3845  keephyp3v  3846  sneqr  4030  preqr1  4036  preq12b  4038  prel12  4039  nfopd  4066  ssex  4426  pwne0  4452  opthwiener  4583  isso2i  4662  ordtri3or  4740  on0eqel  4825  nfimad  5168  dfrel2  5278  funsng  5454  cnvresid  5478  nffvd  5690  fnbrfvb  5722  fvelrnb  5729  fvelimab  5737  funfvop  5805  iunpw  6381  onsucuni  6430  onuninsuci  6442  tposf12  6761  oaword1  6981  oneo  7010  nnaword1  7058  nnneo  7080  inficl  7665  fipwuni  7666  infeq5i  7832  cantnflt  7870  cantnflem1  7887  cantnfltOLD  7900  cantnflem1OLD  7910  cnfcom  7923  cnfcomOLD  7931  rankidn  8019  rankr1id  8059  rankxpsuc  8079  iscard  8135  iscard2  8136  carduni  8141  cardmin2  8158  infxpenlem  8170  alephgeom  8242  cardaleph  8249  infenaleph  8251  iscard3  8253  alephsson  8260  alephfp  8268  alephval3  8270  dfac12k  8306  axdc3lem2  8610  alephval2  8726  alephreg  8736  cfpwsdom  8738  alephom  8739  axrepndlem1  8746  axunndlem1  8749  axunnd  8750  axpowndlem2  8752  axpowndlem2OLD  8753  axpowndlem3  8754  axpowndlem3OLD  8755  axpowndlem4  8756  axpownd  8757  axregndlem2  8759  axinfndlem1  8762  axinfnd  8763  axacndlem4  8767  axacndlem5  8768  axacnd  8769  gchaleph2  8829  elwina  8843  elina  8844  winaon  8845  inawina  8847  winainf  8851  winalim  8852  tskr1om2  8925  r1tskina  8939  gruina  8975  grur1a  8976  indpi  9066  nqerrel  9091  recidnq  9124  ltaddnq  9133  pncan3  9608  divcan2  9992  ltp1  10157  ltm1  10159  recreclt  10221  elnn0z  10649  nn0ind-raph  10732  faclbnd5  12060  hashfun  12185  2swrd2eqwrdeq  12539  caucvgrlem  13136  fsumcnv  13226  ef01bndlem  13453  sin01gt0  13459  cos01gt0  13460  egt2lt3  13473  cnso  13514  4sqlem12  14002  funcres  14791  fuchom  14856  xpsmnd  15446  mulgfval  15610  xpsgrp  15656  nmznsg  15707  symgplusg  15876  frgp0  16239  gsumval3OLD  16364  gsumval3lem1  16365  gsumval3lem2  16366  gsumval3  16367  pwssplit1  17064  mvrf1  17434  blssioo  20216  dvidlem  21234  dvcj  21268  dvrec  21273  rolle  21306  cmvth  21307  mvth  21308  dvlip  21309  dvlipcn  21310  dv11cn  21317  dvivthlem2  21325  lhop1lem  21329  lhop1  21330  lhop2  21331  q1peqb  21513  pserdv  21781  sinhalfpilem  21812  tangtx  21854  logneg2  21951  lgseisenlem4  22578  dchrisum0lem3  22655  mulogsum  22668  pntrlog2bndlem1  22713  axlowdimlem7  23019  axlowdimlem10  23022  axcontlem6  23040  constr3lem2  23357  hsn0elch  24476  axpjcl  24628  omlsilem  24630  pjchi  24660  shs00i  24678  chj00i  24715  chabs1  24744  pjspansn  24805  chscllem1  24865  osumcor2i  24872  nonbooli  24879  atcvat4i  25626  xppreima  25790  xdivrec  25927  sqsscirc1  26194  1stmbfm  26531  2ndmbfm  26532  eulerpartlemgh  26611  cvmlift3lem5  27062  cvmlift3lem7  27064  fprodcnv  27343  dfon2lem3  27447  dfon2lem7  27451  distel  27466  altopthsn  27841  dvasin  28326  areacirclem4  28333  heiborlem8  28563  0rngo  28673  islssfg2  29271  areaquad  29439  stoweidlem13  29656  stoweidlem26  29669  stoweidlem34  29677  wallispilem4  29711  ccatw2s1p1  30117  el2spthonot0  30238  frisusgranb  30437  extwwlkfablem2  30519  bnj981  31685  bnj1148  31729  bnj1154  31732  bj-axc15v  31936  lshpinN  32247  trlid0  33433  hdmap10lem  35100
  Copyright terms: Public domain W3C validator