Theorem mpbii 223

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

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 |- ps
2	1	a1i 11	. 2 |- ( ph -> ps )
3		mpbii.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbid 222	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  elimh  1030  elimhOLD  1033  axc15  2303  ax12v2OLD  2342  eqcomd  2628  eqvisset  3211  vtoclgf  3264  vtoclg1f  3265  eueq3  3381  sbc2or  3444  csbiegf  3557  un00  4011  elimhyp  4146  elimhyp2v  4147  elimhyp3v  4148  elimhyp4v  4149  elimdhyp  4151  keephyp2v  4153  keephyp3v  4154  preqr1OLD  4380  preq12b  4382  prel12  4383  nfopd  4419  ssex  4802  opthwiener  4976  isso2i  5067  nfimad  5475  dfrel2  5583  ordtri3or  5755  on0eqel  5845  funsng  5937  cnvresid  5968  nffvd  6200  fnbrfvb  6236  fvelrnb  6243  fvelimab  6253  funfvop  6329  iunpw  6978  onsucuni  7028  onuninsuci  7040  tposf12  7377  oaword1  7632  oneo  7661  nnaword1  7709  nnneo  7731  inficl  8331  fipwuni  8332  infeq5i  8533  cantnflt  8569  cantnflem1  8586  cnfcom  8597  rankidn  8685  rankr1id  8725  rankxpsuc  8745  iscard  8801  iscard2  8802  carduni  8807  cardmin2  8824  infxpenlem  8836  alephgeom  8905  cardaleph  8912  infenaleph  8914  iscard3  8916  alephsson  8923  alephfp  8931  alephval3  8933  dfac12k  8969  axdc3lem2  9273  alephval2  9394  alephreg  9404  cfpwsdom  9406  alephom  9407  axrepndlem1  9414  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axpownd  9423  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  gchaleph2  9494  elwina  9508  elina  9509  winaon  9510  inawina  9512  winainf  9516  winalim  9517  tskr1om2  9590  r1tskina  9604  gruina  9640  grur1a  9641  indpi  9729  nqerrel  9754  recidnq  9787  ltaddnq  9796  pncan3  10289  divcan2  10693  ltp1  10861  ltm1  10863  recreclt  10922  elnn0z  11390  nn0ind-raph  11477  fzdifsuc  12400  2tnp1ge0ge0  12630  fsuppmapnn0fiubex  12792  faclbnd5  13085  hashfun  13224  ccatalpha  13375  2swrd2eqwrdeq  13696  caucvgrlem  14403  fsumcnv  14504  fprodcnv  14713  ef01bndlem  14914  sin01gt0  14920  cos01gt0  14921  egt2lt3  14934  cnso  14976  ltoddhalfle  15085  4sqlem12  15660  funcres  16556  fuchom  16621  xpsmnd  17330  xpsgrp  17534  mulgfval  17542  nmznsg  17638  symgplusg  17809  frgp0  18173  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  pwssplit1  19059  mvrf1  19425  blssioo  22598  dvidlem  23679  dvcj  23713  dvrec  23718  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  dvlipcn  23757  dv11cn  23764  dvivthlem2  23772  lhop1lem  23776  lhop1  23777  lhop2  23778  q1peqb  23914  pserdv  24183  sinhalfpilem  24215  tangtx  24257  efabl  24296  logneg2  24361  gausslemma2dlem1a  25090  lgseisenlem4  25103  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  dchrisum0lem3  25208  mulogsum  25221  pntrlog2bndlem1  25266  axlowdimlem7  25828  axlowdimlem10  25831  axcontlem6  25849  umgrbi  25996  rusgr1vtxlem  26483  3wlkond  27031  frcond3  27133  hsn0elch  28105  axpjcl  28259  omlsilem  28261  pjchi  28291  shs00i  28309  chj00i  28346  chabs1  28375  pjspansn  28436  chscllem1  28496  osumcor2i  28503  nonbooli  28510  atcvat4i  29256  xppreima  29449  xdivrec  29635  psgndmfi  29846  sqsscirc1  29954  1stmbfm  30322  2ndmbfm  30323  carsgclctunlem2  30381  eulerpartlemgh  30440  hgt750leme  30736  bnj1148  31064  bnj1154  31067  cvmlift3lem5  31305  cvmlift3lem7  31307  logi  31620  dfon2lem3  31690  dfon2lem7  31694  distel  31709  altopthsn  32068  bj-exlimmpbi  32906  poimirlem9  33418  poimirlem26  33435  poimirlem27  33436  poimirlem32  33441  dvasin  33496  areacirclem4  33503  heiborlem8  33617  0rngo  33826  ax12eq  34226  ax12el  34227  ax12inda  34233  ax12v2-o  34234  nfded  34254  nfded2  34255  nfunidALT2  34256  lshpinN  34276  trlid0  35463  hdmap10lem  37131  islssfg2  37641  areaquad  37802  rnmptc  39353  fperdvper  40133  itgvol0  40184  stoweidlem13  40230  stoweidlem26  40243  stoweidlem34  40251  wallispilem4  40285  dirkercncflem1  40320  dirkercncflem3  40322  dirkercncflem4  40323  fourierdlem35  40359  fourierdlem73  40396  lighneallem4b  41526  sbgoldbwt  41665  sbgoldbalt  41669  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem1  41693  bgoldbtbndlem3  41695