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

Theorem mpbii 203
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 11 . 2  |-  ( ph  ->  ps )
3 mpbii.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbid 202 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  elimh  923  ax11v2  2078  ax11v2OLD  2079  sbftOLD  2116  ax11vALT  2173  ax11eq  2270  ax11el  2271  ax11inda  2277  ax11v2-o  2278  vtoclgf  3010  eueq3  3109  moeq3  3111  mo2icl  3113  sbc2or  3169  csbiegf  3291  un00  3663  elimhyp  3787  elimhyp2v  3788  elimhyp3v  3789  elimhyp4v  3790  elimdhyp  3792  keephyp2v  3794  keephyp3v  3795  sneqr  3966  preqr1  3972  preq12b  3974  prel12  3975  nfopd  4001  ssex  4347  opthwiener  4458  isso2i  4535  ordtri3or  4613  on0eqel  4699  iunpw  4759  onsucuni  4808  onuninsuci  4820  nfimad  5212  dfrel2  5321  elxp5  5358  funsng  5497  cnvresid  5523  nffvd  5737  fnbrfvb  5767  fvelrnb  5774  fvelimab  5782  funfvop  5842  tposf12  6504  oaword1  6795  oneo  6824  nnaword1  6872  nnneo  6894  xpsnen  7192  fival  7417  dffi2  7428  inficl  7430  fipwuni  7431  infeq5i  7591  cantnflt  7627  cantnflem1  7645  cnfcom  7657  rankidn  7748  rankr1id  7788  rankxpsuc  7806  iscard  7862  iscard2  7863  carduni  7868  cardmin2  7885  infxpenlem  7895  alephgeom  7963  cardaleph  7970  infenaleph  7972  iscard3  7974  alephsson  7981  alephfp  7989  alephval3  7991  dfac12k  8027  axdc3lem2  8331  alephval2  8447  alephreg  8457  cfpwsdom  8459  alephom  8460  axrepndlem1  8467  axunndlem1  8470  axunnd  8471  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axpownd  8476  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487  gchaleph2  8551  elwina  8561  elina  8562  winaon  8563  inawina  8565  winainf  8569  winalim  8570  tskr1om2  8643  r1tskina  8657  gruina  8693  grur1a  8694  indpi  8784  nqerrel  8809  recidnq  8842  ltaddnq  8851  pncan3  9313  divcan2  9686  ltp1  9848  ltm1  9850  recreclt  9909  elnn0z  10294  nn0ind-raph  10370  faclbnd5  11589  hashfun  11700  caucvgrlem  12466  fsumcnv  12557  ef01bndlem  12785  sin01gt0  12791  cos01gt0  12792  egt2lt3  12805  cnso  12846  4sqlem12  13324  funcres  14093  fuchom  14158  xpsmnd  14735  mulgfval  14891  xpsgrp  14937  nmznsg  14984  symgplusg  15099  frgp0  15392  gsumval3  15514  mvrf1  16489  blssioo  18826  dvidlem  19802  dvcj  19836  dvrec  19841  rolle  19874  cmvth  19875  mvth  19876  dvlip  19877  dvlipcn  19878  dv11cn  19885  dvivthlem2  19893  lhop1lem  19897  lhop1  19898  lhop2  19899  q1peqb  20077  pserdv  20345  sinhalfpilem  20374  tangtx  20413  logneg2  20510  lgseisenlem4  21136  dchrisum0lem3  21213  mulogsum  21226  pntrlog2bndlem1  21271  constr3lem2  21633  hsn0elch  22750  axpjcl  22902  omlsilem  22904  pjchi  22934  shs00i  22952  chj00i  22989  chabs1  23018  pjspansn  23079  chscllem1  23139  osumcor2i  23146  nonbooli  23153  atcvat4i  23900  xppreima  24059  xdivrec  24173  sqsscirc1  24306  1stmbfm  24610  2ndmbfm  24611  cvmlift3lem5  25010  cvmlift3lem7  25012  fprodcnv  25307  dfon2lem3  25412  dfon2lem7  25416  distel  25431  fnimage  25774  altopthsn  25806  axlowdimlem7  25887  axlowdimlem10  25890  axcontlem6  25908  areacirclem4  26295  heiborlem8  26527  0rngo  26637  islssfg2  27146  pwssplit1  27165  stoweidlem13  27738  stoweidlem26  27751  stoweidlem34  27759  wallispilem4  27793  el2spthonot0  28338  frisusgranb  28387  bnj981  29321  bnj1148  29365  bnj1154  29368  ax11v2NEW7  29530  sbftNEW7  29556  lshpinN  29787  trlid0  30973  hdmap10lem  32640
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 178
  Copyright terms: Public domain W3C validator