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  954  ax12vOLD  1805  ax12v2  2056  ax12eq  2264  ax12el  2265  ax12inda  2271  ax12v2-o  2272  eqcomd  2475  eqvisset  3121  vtoclgf  3169  vtoclg1f  3170  eueq3  3278  sbc2or  3340  csbiegf  3459  un00  3862  elimhyp  3998  elimhyp2v  3999  elimhyp3v  4000  elimhyp4v  4001  elimdhyp  4003  keephyp2v  4005  keephyp3v  4006  sneqr  4194  preqr1  4200  preq12b  4202  prel12  4203  nfopd  4230  ssex  4591  pwne0  4617  opthwiener  4749  isso2i  4832  ordtri3or  4910  on0eqel  4995  nfimad  5346  dfrel2  5457  funsng  5634  cnvresid  5658  nffvd  5875  fnbrfvb  5908  fvelrnb  5915  fvelimab  5923  funfvop  5993  iunpw  6598  onsucuni  6647  onuninsuci  6659  tposf12  6980  oaword1  7201  oneo  7230  nnaword1  7278  nnneo  7300  inficl  7885  fipwuni  7886  infeq5i  8053  cantnflt  8091  cantnflem1  8108  cantnfltOLD  8121  cantnflem1OLD  8131  cnfcom  8144  cnfcomOLD  8152  rankidn  8240  rankr1id  8280  rankxpsuc  8300  iscard  8356  iscard2  8357  carduni  8362  cardmin2  8379  infxpenlem  8391  alephgeom  8463  cardaleph  8470  infenaleph  8472  iscard3  8474  alephsson  8481  alephfp  8489  alephval3  8491  dfac12k  8527  axdc3lem2  8831  alephval2  8947  alephreg  8957  cfpwsdom  8959  alephom  8960  axrepndlem1  8967  axunndlem1  8970  axunnd  8971  axpowndlem2  8973  axpowndlem2OLD  8974  axpowndlem3  8975  axpowndlem3OLD  8976  axpowndlem4  8977  axpownd  8978  axregndlem2  8980  axinfndlem1  8983  axinfnd  8984  axacndlem4  8988  axacndlem5  8989  axacnd  8990  gchaleph2  9050  elwina  9064  elina  9065  winaon  9066  inawina  9068  winainf  9072  winalim  9073  tskr1om2  9146  r1tskina  9160  gruina  9196  grur1a  9197  indpi  9285  nqerrel  9310  recidnq  9343  ltaddnq  9352  pncan3  9828  divcan2  10215  ltp1  10380  ltm1  10382  recreclt  10444  elnn0z  10877  nn0ind-raph  10961  fzdifsuc  11739  fsuppmapnn0fiubex  12066  faclbnd5  12344  hashfun  12461  ccatw2s1p1  12603  2swrd2eqwrdeq  12854  caucvgrlem  13458  fsumcnv  13551  ef01bndlem  13780  sin01gt0  13786  cos01gt0  13787  egt2lt3  13800  cnso  13841  4sqlem12  14333  funcres  15123  fuchom  15188  xpsmnd  15779  mulgfval  15953  xpsgrp  15999  nmznsg  16050  symgplusg  16219  frgp0  16584  gsumval3OLD  16711  gsumval3lem1  16712  gsumval3lem2  16713  gsumval3  16714  pwssplit1  17505  mvrf1  17880  blssioo  21063  dvidlem  22082  dvcj  22116  dvrec  22121  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  dvlipcn  22158  dv11cn  22165  dvivthlem2  22173  lhop1lem  22177  lhop1  22178  lhop2  22179  q1peqb  22318  pserdv  22586  sinhalfpilem  22617  tangtx  22659  logneg2  22756  lgseisenlem4  23383  dchrisum0lem3  23460  mulogsum  23473  pntrlog2bndlem1  23518  axlowdimlem7  23955  axlowdimlem10  23958  axcontlem6  23976  constr3lem2  24350  el2spthonot0  24575  frisusgranb  24701  extwwlkfablem2  24783  hsn0elch  25870  axpjcl  26022  omlsilem  26024  pjchi  26054  shs00i  26072  chj00i  26109  chabs1  26138  pjspansn  26199  chscllem1  26259  osumcor2i  26266  nonbooli  26273  atcvat4i  27020  xppreima  27187  xdivrec  27319  sqsscirc1  27554  1stmbfm  27899  2ndmbfm  27900  eulerpartlemgh  27985  cvmlift3lem5  28436  cvmlift3lem7  28438  fprodcnv  28718  dfon2lem3  28822  dfon2lem7  28826  distel  28841  altopthsn  29216  dvasin  29708  areacirclem4  29715  heiborlem8  29945  0rngo  30055  islssfg2  30649  areaquad  30817  stoweidlem13  31341  stoweidlem26  31354  stoweidlem34  31362  wallispilem4  31396  bnj981  33105  bnj1148  33149  bnj1154  33152  bj-elimhyp  33258  bj-axc15v  33429  bj-exlimmpbi  33577  lshpinN  33804  trlid0  34990  hdmap10lem  36657
  Copyright terms: Public domain W3C validator