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  cvmlift3lem5  23265  cvmlift3lem7  23267  dfon2lem3  23552  dfon2lem7  23556  distel  23571  fnimage  23879  altopthsn  23906  axlowdimlem7  23987  axlowdimlem10  23990  axcontlem6  24008  areacirclem5  24341  cur1vald  24611  trooo  24806  trinv  24807  istopx  24959  heiborlem8  25954  0rngo  26064  islssfg2  26581  pwssplit1  26600  stoweidlem13  27174  stoweidlem26  27187  wallispilem4  27229  bnj981  28355  bnj1148  28399  bnj1154  28402  lshpinN  28552  trlid0  29738  hdmap10lem  31405
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