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

Theorem mpbii 215
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 214 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  elimh  965  ax12vOLD  1908  ax12v2  2139  eqcomd  2431  eqvisset  3090  vtoclgf  3138  vtoclg1f  3139  eueq3  3247  sbc2or  3309  csbiegf  3420  un00  3829  elimhyp  3968  elimhyp2v  3969  elimhyp3v  3970  elimhyp4v  3971  elimdhyp  3973  keephyp2v  3975  keephyp3v  3976  sneqr  4165  preqr1  4172  preq12b  4174  prel12  4175  nfopd  4202  ssex  4566  pwne0  4592  opthwiener  4720  isso2i  4804  nfimad  5194  dfrel2  5303  ordtri3or  5472  on0eqel  5557  funsng  5645  cnvresid  5669  nffvd  5888  fnbrfvb  5919  fvelrnb  5926  fvelimab  5935  funfvop  6007  iunpw  6617  onsucuni  6667  onuninsuci  6679  tposf12  7004  oaword1  7259  oneo  7288  nnaword1  7336  nnneo  7358  inficl  7943  fipwuni  7944  infeq5i  8145  cantnflt  8180  cantnflem1  8197  cnfcom  8208  rankidn  8296  rankr1id  8336  rankxpsuc  8356  iscard  8412  iscard2  8413  carduni  8418  cardmin2  8435  infxpenlem  8447  alephgeom  8515  cardaleph  8522  infenaleph  8524  iscard3  8526  alephsson  8533  alephfp  8541  alephval3  8543  dfac12k  8579  axdc3lem2  8883  alephval2  8999  alephreg  9009  cfpwsdom  9011  alephom  9012  axrepndlem1  9019  axunndlem1  9022  axunnd  9023  axpowndlem2  9025  axpowndlem3  9026  axpowndlem4  9027  axpownd  9028  axregndlem2  9030  axinfndlem1  9032  axinfnd  9033  axacndlem4  9037  axacndlem5  9038  axacnd  9039  gchaleph2  9099  elwina  9113  elina  9114  winaon  9115  inawina  9117  winainf  9121  winalim  9122  tskr1om2  9195  r1tskina  9209  gruina  9245  grur1a  9246  indpi  9334  nqerrel  9359  recidnq  9392  ltaddnq  9401  pncan3  9885  divcan2  10280  ltp1  10445  ltm1  10447  recreclt  10507  elnn0z  10952  nn0ind-raph  11037  fzdifsuc  11857  fsuppmapnn0fiubex  12205  faclbnd5  12484  hashfun  12608  2swrd2eqwrdeq  13022  caucvgrlem  13729  caucvgrlemOLD  13730  fsumcnv  13827  fprodcnv  14030  ef01bndlem  14231  sin01gt0  14237  cos01gt0  14238  egt2lt3  14251  cnso  14292  4sqlem12  14893  funcres  15794  fuchom  15859  xpsmnd  16569  mulgfval  16752  xpsgrp  16798  nmznsg  16854  symgplusg  17023  frgp0  17403  gsumval3lem1  17532  gsumval3lem2  17533  gsumval3  17534  pwssplit1  18275  mvrf1  18642  blssioo  21805  dvidlem  22862  dvcj  22896  dvrec  22901  rolle  22934  cmvth  22935  mvth  22936  dvlip  22937  dvlipcn  22938  dv11cn  22945  dvivthlem2  22953  lhop1lem  22957  lhop1  22958  lhop2  22959  q1peqb  23097  pserdv  23376  sinhalfpilem  23410  tangtx  23452  efabl  23491  logneg2  23556  lgseisenlem4  24272  dchrisum0lem3  24349  mulogsum  24362  pntrlog2bndlem1  24407  axlowdimlem7  24970  axlowdimlem10  24973  axcontlem6  24991  constr3lem2  25366  el2spthonot0  25591  frisusgranb  25717  extwwlkfablem2  25798  hsn0elch  26893  axpjcl  27045  omlsilem  27047  pjchi  27077  shs00i  27095  chj00i  27132  chabs1  27161  pjspansn  27222  chscllem1  27282  osumcor2i  27289  nonbooli  27296  atcvat4i  28042  xppreima  28244  xdivrec  28397  psgndmfi  28611  sqsscirc1  28716  1stmbfm  29084  2ndmbfm  29085  carsgclctunlem2  29153  eulerpartlemgh  29213  bnj1148  29807  bnj1154  29810  cvmlift3lem5  30048  cvmlift3lem7  30050  logi  30371  dfon2lem3  30432  dfon2lem7  30436  distel  30451  altopthsn  30727  bj-elimhyp  31152  bj-axc15v  31323  bj-exlimmpbi  31476  wl-ax12v3  31870  poimirlem9  31907  poimirlem26  31924  poimirlem27  31925  poimirlem32  31930  dvasin  31986  areacirclem4  31993  heiborlem8  32108  0rngo  32218  ax12eq  32475  ax12el  32476  ax12inda  32482  ax12v2-o  32483  lshpinN  32518  trlid0  33705  hdmap10lem  35373  islssfg2  35893  areaquad  36065  rnmptc  37330  fperdvper  37654  itgvol0  37709  stoweidlem13  37737  stoweidlem26  37750  stoweidlem34  37759  wallispilem4  37794  dirkercncflem1  37829  dirkercncflem3  37831  dirkercncflem4  37832  fourierdlem35  37869  fourierdlem73  37907  bgoldbwt  38634  sgoldbalt  38638  nnsum4primeseven  38651  nnsum4primesevenALTV  38652  bgoldbtbndlem1  38656  bgoldbtbndlem3  38658
  Copyright terms: Public domain W3C validator