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  947  ax12v2  2033  ax12vALT  2131  ax12eq  2242  ax12el  2243  ax12inda  2249  ax12v2-o  2250  eqvisset  2980  vtoclgf  3028  vtoclg1f  3029  eueq3  3134  sbc2or  3195  csbiegf  3312  un00  3714  elimhyp  3848  elimhyp2v  3849  elimhyp3v  3850  elimhyp4v  3851  elimdhyp  3853  keephyp2v  3855  keephyp3v  3856  sneqr  4040  preqr1  4046  preq12b  4048  prel12  4049  nfopd  4076  ssex  4436  pwne0  4462  opthwiener  4593  isso2i  4673  ordtri3or  4751  on0eqel  4836  nfimad  5178  dfrel2  5288  funsng  5464  cnvresid  5488  nffvd  5700  fnbrfvb  5732  fvelrnb  5739  fvelimab  5747  funfvop  5815  iunpw  6390  onsucuni  6439  onuninsuci  6451  tposf12  6770  oaword1  6991  oneo  7020  nnaword1  7068  nnneo  7090  inficl  7675  fipwuni  7676  infeq5i  7842  cantnflt  7880  cantnflem1  7897  cantnfltOLD  7910  cantnflem1OLD  7920  cnfcom  7933  cnfcomOLD  7941  rankidn  8029  rankr1id  8069  rankxpsuc  8089  iscard  8145  iscard2  8146  carduni  8151  cardmin2  8168  infxpenlem  8180  alephgeom  8252  cardaleph  8259  infenaleph  8261  iscard3  8263  alephsson  8270  alephfp  8278  alephval3  8280  dfac12k  8316  axdc3lem2  8620  alephval2  8736  alephreg  8746  cfpwsdom  8748  alephom  8749  axrepndlem1  8756  axunndlem1  8759  axunnd  8760  axpowndlem2  8762  axpowndlem2OLD  8763  axpowndlem3  8764  axpowndlem3OLD  8765  axpowndlem4  8766  axpownd  8767  axregndlem2  8769  axinfndlem1  8772  axinfnd  8773  axacndlem4  8777  axacndlem5  8778  axacnd  8779  gchaleph2  8839  elwina  8853  elina  8854  winaon  8855  inawina  8857  winainf  8861  winalim  8862  tskr1om2  8935  r1tskina  8949  gruina  8985  grur1a  8986  indpi  9076  nqerrel  9101  recidnq  9134  ltaddnq  9143  pncan3  9618  divcan2  10002  ltp1  10167  ltm1  10169  recreclt  10231  elnn0z  10659  nn0ind-raph  10742  fzdifsuc  11516  faclbnd5  12074  hashfun  12199  2swrd2eqwrdeq  12553  caucvgrlem  13150  fsumcnv  13240  ef01bndlem  13468  sin01gt0  13474  cos01gt0  13475  egt2lt3  13488  cnso  13529  4sqlem12  14017  funcres  14806  fuchom  14871  xpsmnd  15461  mulgfval  15628  xpsgrp  15674  nmznsg  15725  symgplusg  15894  frgp0  16257  gsumval3OLD  16382  gsumval3lem1  16383  gsumval3lem2  16384  gsumval3  16385  pwssplit1  17140  mvrf1  17498  blssioo  20372  dvidlem  21390  dvcj  21424  dvrec  21429  rolle  21462  cmvth  21463  mvth  21464  dvlip  21465  dvlipcn  21466  dv11cn  21473  dvivthlem2  21481  lhop1lem  21485  lhop1  21486  lhop2  21487  q1peqb  21626  pserdv  21894  sinhalfpilem  21925  tangtx  21967  logneg2  22064  lgseisenlem4  22691  dchrisum0lem3  22768  mulogsum  22781  pntrlog2bndlem1  22826  axlowdimlem7  23194  axlowdimlem10  23197  axcontlem6  23215  constr3lem2  23532  hsn0elch  24651  axpjcl  24803  omlsilem  24805  pjchi  24835  shs00i  24853  chj00i  24890  chabs1  24919  pjspansn  24980  chscllem1  25040  osumcor2i  25047  nonbooli  25054  atcvat4i  25801  xppreima  25964  xdivrec  26102  sqsscirc1  26338  1stmbfm  26675  2ndmbfm  26676  eulerpartlemgh  26761  cvmlift3lem5  27212  cvmlift3lem7  27214  fprodcnv  27494  dfon2lem3  27598  dfon2lem7  27602  distel  27617  altopthsn  27992  dvasin  28480  areacirclem4  28487  heiborlem8  28717  0rngo  28827  islssfg2  29424  areaquad  29592  stoweidlem13  29808  stoweidlem26  29821  stoweidlem34  29829  wallispilem4  29863  ccatw2s1p1  30269  el2spthonot0  30390  frisusgranb  30589  extwwlkfablem2  30671  fsuppmapnn0fiubex  30800  bnj981  31943  bnj1148  31987  bnj1154  31990  bj-elimhyp  32096  bj-axc15v  32265  bj-exlimmpbi  32413  lshpinN  32634  trlid0  33820  hdmap10lem  35487
  Copyright terms: Public domain W3C validator