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  1964  sbft  1997  ax11vALT  2069  ax11eq  2165  ax11el  2166  ax11inda  2172  ax11v2-o  2173  vtoclgf  2876  eueq3  2974  moeq3  2976  mo2icl  2978  sbc2or  3033  csbiegf  3155  un00  3524  elimhyp  3647  elimhyp2v  3648  elimhyp3v  3649  elimhyp4v  3650  elimdhyp  3652  keephyp2v  3654  keephyp3v  3655  sneqr  3817  preqr1  3823  preq12b  3825  prel12  3826  nfopd  3850  ssex  4195  opthwiener  4305  isso2i  4383  ordtri3or  4461  on0eqel  4547  iunpw  4607  onsucuni  4656  onuninsuci  4668  nfimad  5058  dfrel2  5161  elxp5  5198  funsng  5335  cnvresid  5359  nffvd  5572  fnbrfvb  5601  fvelrnb  5608  fvelimab  5616  funfvop  5675  tposss  6277  tposf12  6301  oaword1  6592  oneo  6621  nnaword1  6669  nnneo  6691  xpsnen  6989  sbthlem5  7018  fival  7211  dffi2  7221  inficl  7223  fipwuni  7224  infeq5i  7382  cantnflt  7418  cantnflem1  7436  cnfcom  7448  rankidn  7539  rankr1id  7579  rankxpsuc  7597  iscard  7653  iscard2  7654  carduni  7659  cardmin2  7676  infxpenlem  7686  alephgeom  7754  cardaleph  7761  infenaleph  7763  iscard3  7765  alephsson  7772  alephfp  7780  alephval3  7782  dfac12k  7818  axdc3lem2  8122  alephval2  8239  alephreg  8249  cfpwsdom  8251  alephom  8252  axrepndlem1  8259  axunndlem1  8262  axunnd  8263  axpowndlem2  8265  axpowndlem3  8266  axpowndlem4  8267  axpownd  8268  axregndlem2  8270  axinfndlem1  8272  axinfnd  8273  axacndlem4  8277  axacndlem5  8278  axacnd  8279  gchaleph2  8343  elwina  8353  elina  8354  winaon  8355  inawina  8357  winainf  8361  winalim  8362  tskr1om2  8435  r1tskina  8449  gruina  8485  grur1a  8486  indpi  8576  nqerrel  8601  recidnq  8634  ltaddnq  8643  pncan3  9104  divcan2  9477  ltp1  9639  ltm1  9641  recreclt  9700  elnn0z  10083  nn0ind-raph  10159  faclbnd5  11358  hashfun  11436  caucvgrlem  12192  fsumcnv  12283  ef01bndlem  12511  sin01gt0  12517  cos01gt0  12518  egt2lt3  12531  cnso  12572  4sqlem12  13050  funcres  13819  fuchom  13884  xpsmnd  14461  mulgfval  14617  xpsgrp  14663  nmznsg  14710  symgplusg  14825  frgp0  15118  gsumval3  15240  mvrf1  16219  cnclsi  17057  txss12  17356  txbasval  17357  kqsat  17478  kqcldsat  17480  blssioo  18353  dvidlem  19318  dvcj  19352  dvrec  19357  rolle  19390  cmvth  19391  mvth  19392  dvlip  19393  dvlipcn  19394  dv11cn  19401  dvivthlem2  19409  lhop1lem  19413  lhop1  19414  lhop2  19415  q1peqb  19593  pserdv  19858  sinhalfpilem  19887  tangtx  19926  logneg2  20022  dchrelbas2  20529  lgseisenlem4  20644  dchrisum0lem3  20721  mulogsum  20734  pntrlog2bndlem1  20779  hsn0elch  21882  axpjcl  22034  omlsilem  22036  chsupsn  22047  pjchi  22066  shs00i  22084  chj00i  22121  chabs1  22150  pjspansn  22211  chscllem1  22271  osumcor2i  22278  nonbooli  22285  pjss1coi  22798  atcvat4i  23032  xppreima  23208  xdivrec  23325  sqsscirc1  23375  sigagensiga  23700  1stmbfm  23784  2ndmbfm  23785  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemi1  23934  ballotlemii  23935  ballotlemic  23938  ballotlem1c  23939  cvmlift3lem5  24138  cvmlift3lem7  24140  dfon2lem3  24526  dfon2lem7  24530  distel  24545  fnimage  24853  altopthsn  24881  axlowdimlem7  24962  axlowdimlem10  24965  axcontlem6  24983  areacirclem5  25346  heiborlem8  25690  0rngo  25800  islssfg2  26317  pwssplit1  26336  stoweidlem13  26910  stoweidlem26  26923  wallispilem4  26965  constr3lem2  27530  frisusgranb  27589  bnj981  28493  bnj1148  28537  bnj1154  28540  ax11v2NEW7  28700  sbftNEW7  28726  lshpinN  28997  trlid0  30183  hdmap10lem  31850
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