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

Theorem mpbii 202
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-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 10 . 2  |-  ( ph  ->  ps )
3 mpbii.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbid 201 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  elimh  922  ax11v2  1932  sbft  1965  ax11eq  2132  ax11el  2133  ax11inda  2139  ax11v2-o  2140  vtoclgf  2842  eueq3  2940  moeq3  2942  mo2icl  2944  sbc2or  2999  csbiegf  3121  un00  3490  elimhyp  3613  elimhyp2v  3614  elimhyp3v  3615  elimhyp4v  3616  elimdhyp  3618  keephyp2v  3620  keephyp3v  3621  sneqr  3780  preqr1  3786  preq12b  3788  prel12  3789  nfopd  3813  ssex  4158  opthwiener  4268  isso2i  4346  ordtri3or  4424  on0eqel  4510  iunpw  4570  onsucuni  4619  onuninsuci  4631  nfimad  5021  dfrel2  5124  elxp5  5161  funsng  5298  cnvresid  5322  nffvd  5534  fnbrfvb  5563  fvelrnb  5570  fvelimab  5578  funfvop  5637  tposss  6235  tposf12  6259  oaword1  6550  oneo  6579  nnaword1  6627  nnneo  6649  xpsnen  6946  sbthlem5  6975  fival  7166  dffi2  7176  inficl  7178  fipwuni  7179  infeq5i  7337  cantnflt  7373  cantnflem1  7391  cnfcom  7403  rankidn  7494  rankr1id  7534  rankxpsuc  7552  iscard  7608  iscard2  7609  carduni  7614  cardmin2  7631  infxpenlem  7641  alephgeom  7709  cardaleph  7716  infenaleph  7718  iscard3  7720  alephsson  7727  alephfp  7735  alephval3  7737  dfac12k  7773  axdc3lem2  8077  alephval2  8194  alephreg  8204  cfpwsdom  8206  alephom  8207  axrepndlem1  8214  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  gchaleph2  8298  elwina  8308  elina  8309  winaon  8310  inawina  8312  winainf  8316  winalim  8317  tskr1om2  8390  r1tskina  8404  gruina  8440  grur1a  8441  indpi  8531  nqerrel  8556  recidnq  8589  ltaddnq  8598  pncan3  9059  divcan2  9432  ltp1  9594  ltm1  9596  recreclt  9655  elnn0z  10036  nn0ind-raph  10112  faclbnd5  11311  hashfun  11389  caucvgrlem  12145  fsumcnv  12236  ef01bndlem  12464  sin01gt0  12470  cos01gt0  12471  egt2lt3  12484  cnso  12525  4sqlem12  13003  funcres  13770  fuchom  13835  xpsmnd  14412  mulgfval  14568  xpsgrp  14614  nmznsg  14661  symgplusg  14776  frgp0  15069  gsumval3  15191  mvrf1  16170  cnclsi  17001  txss12  17300  txbasval  17301  kqsat  17422  kqcldsat  17424  blssioo  18301  dvidlem  19265  dvcj  19299  dvrec  19304  rolle  19337  cmvth  19338  mvth  19339  dvlip  19340  dvlipcn  19341  dv11cn  19348  dvivthlem2  19356  lhop1lem  19360  lhop1  19361  lhop2  19362  q1peqb  19540  pserdv  19805  sinhalfpilem  19834  tangtx  19873  logneg2  19969  dchrelbas2  20476  lgseisenlem4  20591  dchrisum0lem3  20668  mulogsum  20681  pntrlog2bndlem1  20726  hsn0elch  21827  axpjcl  21979  omlsilem  21981  chsupsn  21992  pjchi  22011  shs00i  22029  chj00i  22066  chabs1  22095  pjspansn  22156  chscllem1  22216  osumcor2i  22223  nonbooli  22230  pjss1coi  22743  atcvat4i  22977  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  xdivrec  23110  xppreima  23211  sqsscirc1  23292  sigagensiga  23502  1stmbfm  23565  2ndmbfm  23566  cvmlift3lem5  23854  cvmlift3lem7  23856  dfon2lem3  24141  dfon2lem7  24145  distel  24160  fnimage  24468  altopthsn  24495  axlowdimlem7  24576  axlowdimlem10  24579  axcontlem6  24597  areacirclem5  24929  cur1vald  25199  trooo  25394  trinv  25395  istopx  25547  heiborlem8  26542  0rngo  26652  islssfg2  27169  pwssplit1  27188  stoweidlem13  27762  stoweidlem26  27775  wallispilem4  27817  bnj981  28982  bnj1148  29026  bnj1154  29029  lshpinN  29179  trlid0  30365  hdmap10lem  32032
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator