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  957  ax12vOLD  1880  ax12v2  2109  eqcomd  2410  eqvisset  3066  vtoclgf  3114  vtoclg1f  3115  eueq3  3223  sbc2or  3285  csbiegf  3396  un00  3804  elimhyp  3942  elimhyp2v  3943  elimhyp3v  3944  elimhyp4v  3945  elimdhyp  3947  keephyp2v  3949  keephyp3v  3950  sneqr  4138  preqr1  4145  preq12b  4147  prel12  4148  nfopd  4175  ssex  4537  pwne0  4563  opthwiener  4691  isso2i  4775  nfimad  5165  dfrel2  5273  ordtri3or  5441  on0eqel  5526  funsng  5614  cnvresid  5638  nffvd  5857  fnbrfvb  5888  fvelrnb  5895  fvelimab  5904  funfvop  5976  iunpw  6595  onsucuni  6645  onuninsuci  6657  tposf12  6982  oaword1  7237  oneo  7266  nnaword1  7314  nnneo  7336  inficl  7918  fipwuni  7919  infeq5i  8085  cantnflt  8122  cantnflem1  8139  cantnfltOLD  8152  cantnflem1OLD  8162  cnfcom  8175  cnfcomOLD  8183  rankidn  8271  rankr1id  8311  rankxpsuc  8331  iscard  8387  iscard2  8388  carduni  8393  cardmin2  8410  infxpenlem  8422  alephgeom  8494  cardaleph  8501  infenaleph  8503  iscard3  8505  alephsson  8512  alephfp  8520  alephval3  8522  dfac12k  8558  axdc3lem2  8862  alephval2  8978  alephreg  8988  cfpwsdom  8990  alephom  8991  axrepndlem1  8998  axunndlem1  9001  axunnd  9002  axpowndlem2  9004  axpowndlem3  9005  axpowndlem4  9006  axpownd  9007  axregndlem2  9009  axinfndlem1  9012  axinfnd  9013  axacndlem4  9017  axacndlem5  9018  axacnd  9019  gchaleph2  9079  elwina  9093  elina  9094  winaon  9095  inawina  9097  winainf  9101  winalim  9102  tskr1om2  9175  r1tskina  9189  gruina  9225  grur1a  9226  indpi  9314  nqerrel  9339  recidnq  9372  ltaddnq  9381  pncan3  9863  divcan2  10255  ltp1  10420  ltm1  10422  recreclt  10483  elnn0z  10917  nn0ind-raph  11002  fzdifsuc  11792  fsuppmapnn0fiubex  12140  faclbnd5  12418  hashfun  12542  2swrd2eqwrdeq  12945  caucvgrlem  13642  fsumcnv  13737  fprodcnv  13937  ef01bndlem  14126  sin01gt0  14132  cos01gt0  14133  egt2lt3  14146  cnso  14187  4sqlem12  14681  funcres  15507  fuchom  15572  xpsmnd  16282  mulgfval  16465  xpsgrp  16511  nmznsg  16567  symgplusg  16736  frgp0  17100  gsumval3OLD  17230  gsumval3lem1  17231  gsumval3lem2  17232  gsumval3  17233  pwssplit1  18023  mvrf1  18399  blssioo  21590  dvidlem  22609  dvcj  22643  dvrec  22648  rolle  22681  cmvth  22682  mvth  22683  dvlip  22684  dvlipcn  22685  dv11cn  22692  dvivthlem2  22700  lhop1lem  22704  lhop1  22705  lhop2  22706  q1peqb  22845  pserdv  23114  sinhalfpilem  23146  tangtx  23188  efabl  23227  logneg2  23292  lgseisenlem4  24006  dchrisum0lem3  24083  mulogsum  24096  pntrlog2bndlem1  24141  axlowdimlem7  24655  axlowdimlem10  24658  axcontlem6  24676  constr3lem2  25050  el2spthonot0  25275  frisusgranb  25401  extwwlkfablem2  25482  hsn0elch  26566  axpjcl  26718  omlsilem  26720  pjchi  26750  shs00i  26768  chj00i  26805  chabs1  26834  pjspansn  26895  chscllem1  26955  osumcor2i  26962  nonbooli  26969  atcvat4i  27715  xppreima  27916  xdivrec  28061  sqsscirc1  28329  1stmbfm  28694  2ndmbfm  28695  carsgclctunlem2  28753  eulerpartlemgh  28809  bnj1148  29366  bnj1154  29369  cvmlift3lem5  29607  cvmlift3lem7  29609  logi  29930  dfon2lem3  29991  dfon2lem7  29995  distel  30010  altopthsn  30286  bj-elimhyp  30711  bj-axc15v  30881  bj-exlimmpbi  31029  dvasin  31454  areacirclem4  31461  heiborlem8  31576  0rngo  31686  ax12eq  31944  ax12el  31945  ax12inda  31951  ax12v2-o  31952  lshpinN  31987  trlid0  33174  hdmap10lem  34842  islssfg2  35359  areaquad  35528  rnmptc  36804  fperdvper  37064  itgvol0  37116  stoweidlem13  37144  stoweidlem26  37157  stoweidlem34  37165  wallispilem4  37199  dirkercncflem1  37234  dirkercncflem3  37236  dirkercncflem4  37237  fourierdlem35  37273  fourierdlem73  37311  bgoldbwt  37812  sgoldbalt  37816  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  bgoldbtbndlem1  37834  bgoldbtbndlem3  37836
  Copyright terms: Public domain W3C validator