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  1945  sbft  1978  ax11eq  2145  ax11el  2146  ax11inda  2152  ax11v2-o  2153  vtoclgf  2855  eueq3  2953  moeq3  2955  mo2icl  2957  sbc2or  3012  csbiegf  3134  un00  3503  elimhyp  3626  elimhyp2v  3627  elimhyp3v  3628  elimhyp4v  3629  elimdhyp  3631  keephyp2v  3633  keephyp3v  3634  sneqr  3796  preqr1  3802  preq12b  3804  prel12  3805  nfopd  3829  ssex  4174  opthwiener  4284  isso2i  4362  ordtri3or  4440  on0eqel  4526  iunpw  4586  onsucuni  4635  onuninsuci  4647  nfimad  5037  dfrel2  5140  elxp5  5177  funsng  5314  cnvresid  5338  nffvd  5550  fnbrfvb  5579  fvelrnb  5586  fvelimab  5594  funfvop  5653  tposss  6251  tposf12  6275  oaword1  6566  oneo  6595  nnaword1  6643  nnneo  6665  xpsnen  6962  sbthlem5  6991  fival  7182  dffi2  7192  inficl  7194  fipwuni  7195  infeq5i  7353  cantnflt  7389  cantnflem1  7407  cnfcom  7419  rankidn  7510  rankr1id  7550  rankxpsuc  7568  iscard  7624  iscard2  7625  carduni  7630  cardmin2  7647  infxpenlem  7657  alephgeom  7725  cardaleph  7732  infenaleph  7734  iscard3  7736  alephsson  7743  alephfp  7751  alephval3  7753  dfac12k  7789  axdc3lem2  8093  alephval2  8210  alephreg  8220  cfpwsdom  8222  alephom  8223  axrepndlem1  8230  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axpownd  8239  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  gchaleph2  8314  elwina  8324  elina  8325  winaon  8326  inawina  8328  winainf  8332  winalim  8333  tskr1om2  8406  r1tskina  8420  gruina  8456  grur1a  8457  indpi  8547  nqerrel  8572  recidnq  8605  ltaddnq  8614  pncan3  9075  divcan2  9448  ltp1  9610  ltm1  9612  recreclt  9671  elnn0z  10052  nn0ind-raph  10128  faclbnd5  11327  hashfun  11405  caucvgrlem  12161  fsumcnv  12252  ef01bndlem  12480  sin01gt0  12486  cos01gt0  12487  egt2lt3  12500  cnso  12541  4sqlem12  13019  funcres  13786  fuchom  13851  xpsmnd  14428  mulgfval  14584  xpsgrp  14630  nmznsg  14677  symgplusg  14792  frgp0  15085  gsumval3  15207  mvrf1  16186  cnclsi  17017  txss12  17316  txbasval  17317  kqsat  17438  kqcldsat  17440  blssioo  18317  dvidlem  19281  dvcj  19315  dvrec  19320  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  dv11cn  19364  dvivthlem2  19372  lhop1lem  19376  lhop1  19377  lhop2  19378  q1peqb  19556  pserdv  19821  sinhalfpilem  19850  tangtx  19889  logneg2  19985  dchrelbas2  20492  lgseisenlem4  20607  dchrisum0lem3  20684  mulogsum  20697  pntrlog2bndlem1  20742  hsn0elch  21843  axpjcl  21995  omlsilem  21997  chsupsn  22008  pjchi  22027  shs00i  22045  chj00i  22082  chabs1  22111  pjspansn  22172  chscllem1  22232  osumcor2i  22239  nonbooli  22246  pjss1coi  22759  atcvat4i  22993  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  xdivrec  23126  xppreima  23226  sqsscirc1  23307  sigagensiga  23517  1stmbfm  23580  2ndmbfm  23581  cvmlift3lem5  23869  cvmlift3lem7  23871  dfon2lem3  24212  dfon2lem7  24216  distel  24231  fnimage  24539  altopthsn  24567  axlowdimlem7  24648  axlowdimlem10  24651  axcontlem6  24669  areacirclem5  25032  cur1vald  25302  trooo  25497  trinv  25498  istopx  25650  heiborlem8  26645  0rngo  26755  islssfg2  27272  pwssplit1  27291  stoweidlem13  27865  stoweidlem26  27878  wallispilem4  27920  constr3lem2  28392  bnj981  29298  bnj1148  29342  bnj1154  29345  ax11v2NEW7  29505  sbftNEW7  29531  lshpinN  29801  trlid0  30987  hdmap10lem  32654
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