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

Theorem mpbii 216
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 215 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  elimh  1000  elimhOLD  1003  axc15  2153  ax12v2OLD  2191  eqcomd  2477  eqvisset  3039  vtoclgf  3091  vtoclg1f  3092  eueq3  3201  sbc2or  3264  csbiegf  3373  un00  3804  elimhyp  3930  elimhyp2v  3931  elimhyp3v  3932  elimhyp4v  3933  elimdhyp  3935  keephyp2v  3937  keephyp3v  3938  sneqr  4131  preqr1OLD  4140  preq12b  4142  prel12  4143  nfopd  4175  ssex  4540  pwne0  4571  opthwiener  4703  isso2i  4792  nfimad  5183  dfrel2  5292  ordtri3or  5462  on0eqel  5547  funsng  5635  cnvresid  5663  nffvd  5888  fnbrfvb  5919  fvelrnb  5926  fvelimab  5936  funfvop  6009  iunpw  6624  onsucuni  6674  onuninsuci  6686  tposf12  7016  oaword1  7271  oneo  7300  nnaword1  7348  nnneo  7370  inficl  7957  fipwuni  7958  infeq5i  8159  cantnflt  8195  cantnflem1  8212  cnfcom  8223  rankidn  8311  rankr1id  8351  rankxpsuc  8371  iscard  8427  iscard2  8428  carduni  8433  cardmin2  8450  infxpenlem  8462  alephgeom  8531  cardaleph  8538  infenaleph  8540  iscard3  8542  alephsson  8549  alephfp  8557  alephval3  8559  dfac12k  8595  axdc3lem2  8899  alephval2  9015  alephreg  9025  cfpwsdom  9027  alephom  9028  axrepndlem1  9035  axunndlem1  9038  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axpownd  9044  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  gchaleph2  9115  elwina  9129  elina  9130  winaon  9131  inawina  9133  winainf  9137  winalim  9138  tskr1om2  9211  r1tskina  9225  gruina  9261  grur1a  9262  indpi  9350  nqerrel  9375  recidnq  9408  ltaddnq  9417  pncan3  9903  divcan2  10300  ltp1  10465  ltm1  10467  recreclt  10527  elnn0z  10974  nn0ind-raph  11058  fzdifsuc  11881  fsuppmapnn0fiubex  12242  faclbnd5  12521  hashfun  12650  ccatalpha  12787  2swrd2eqwrdeq  13103  caucvgrlem  13813  caucvgrlemOLD  13814  fsumcnv  13911  fprodcnv  14114  ef01bndlem  14315  sin01gt0  14321  cos01gt0  14322  egt2lt3  14335  cnso  14376  4sqlem12  14979  funcres  15879  fuchom  15944  xpsmnd  16654  mulgfval  16837  xpsgrp  16883  nmznsg  16939  symgplusg  17108  frgp0  17488  gsumval3lem1  17617  gsumval3lem2  17618  gsumval3  17619  pwssplit1  18360  mvrf1  18726  blssioo  21891  dvidlem  22949  dvcj  22983  dvrec  22988  rolle  23021  cmvth  23022  mvth  23023  dvlip  23024  dvlipcn  23025  dv11cn  23032  dvivthlem2  23040  lhop1lem  23044  lhop1  23045  lhop2  23046  q1peqb  23184  pserdv  23463  sinhalfpilem  23497  tangtx  23539  efabl  23578  logneg2  23643  lgseisenlem4  24359  dchrisum0lem3  24436  mulogsum  24449  pntrlog2bndlem1  24494  axlowdimlem7  25057  axlowdimlem10  25060  axcontlem6  25078  constr3lem2  25453  el2spthonot0  25678  frisusgranb  25804  extwwlkfablem2  25885  hsn0elch  26982  axpjcl  27134  omlsilem  27136  pjchi  27166  shs00i  27184  chj00i  27221  chabs1  27250  pjspansn  27311  chscllem1  27371  osumcor2i  27378  nonbooli  27385  atcvat4i  28131  xppreima  28324  xdivrec  28471  psgndmfi  28683  sqsscirc1  28788  1stmbfm  29155  2ndmbfm  29156  carsgclctunlem2  29224  eulerpartlemgh  29284  bnj1148  29877  bnj1154  29880  cvmlift3lem5  30118  cvmlift3lem7  30120  logi  30441  dfon2lem3  30502  dfon2lem7  30506  distel  30521  altopthsn  30799  bj-axc15v  31428  bj-exlimmpbi  31581  poimirlem9  32013  poimirlem26  32030  poimirlem27  32031  poimirlem32  32036  dvasin  32092  areacirclem4  32099  heiborlem8  32214  0rngo  32324  ax12eq  32576  ax12el  32577  ax12inda  32583  ax12v2-o  32584  nfded  32604  nfded2  32605  nfunidALT2  32606  lshpinN  32626  trlid0  33813  hdmap10lem  35481  islssfg2  36000  areaquad  36172  rnmptc  37510  fperdvper  37887  itgvol0  37942  stoweidlem13  37985  stoweidlem26  37998  stoweidlem34  38007  wallispilem4  38042  dirkercncflem1  38077  dirkercncflem3  38079  dirkercncflem4  38080  fourierdlem35  38117  fourierdlem73  38155  bgoldbwt  39023  sgoldbalt  39027  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbndlem1  39045  bgoldbtbndlem3  39047  umgrbi  39346  rusgr1vtxlem  39791  31wlkond  40085
  Copyright terms: Public domain W3C validator