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

Theorem mpbii 205
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
mpbii.maj
Assertion
Ref Expression
mpbii

Proof of Theorem mpbii
StepHypRef Expression
1 mpbii.min . . 3
21a1i 11 . 2
3 mpbii.maj . 2
42, 3mpbid 204 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  elimh  932  ax12v2  2024  ax12vALT  2123  ax12eq  2233  ax12el  2234  ax12inda  2240  ax12v2-o  2241  eqvisset  2959  vtoclgf  3006  vtoclg1f  3007  eueq3  3112  sbc2or  3172  csbiegf  3289  un00  3691  elimhyp  3825  elimhyp2v  3826  elimhyp3v  3827  elimhyp4v  3828  elimdhyp  3830  keephyp2v  3832  keephyp3v  3833  sneqr  4015  preqr1  4021  preq12b  4023  prel12  4024  nfopd  4051  ssex  4411  pwne0  4434  opthwiener  4565  isso2i  4644  ordtri3or  4722  on0eqel  4807  nfimad  5150  dfrel2  5260  funsng  5434  cnvresid  5458  nffvd  5670  fnbrfvb  5702  fvelrnb  5709  fvelimab  5717  funfvop  5785  iunpw  6360  onsucuni  6409  onuninsuci  6421  tposf12  6732  oaword1  6952  oneo  6981  nnaword1  7029  nnneo  7051  inficl  7622  fipwuni  7623  infeq5i  7789  cantnflt  7827  cantnflem1  7844  cantnfltOLD  7857  cantnflem1OLD  7867  cnfcom  7880  cnfcomOLD  7888  rankidn  7976  rankr1id  8016  rankxpsuc  8036  iscard  8092  iscard2  8093  carduni  8098  cardmin2  8115  infxpenlem  8127  alephgeom  8199  cardaleph  8206  infenaleph  8208  iscard3  8210  alephsson  8217  alephfp  8225  alephval3  8227  dfac12k  8263  axdc3lem2  8567  alephval2  8683  alephreg  8693  cfpwsdom  8695  alephom  8696  axrepndlem1  8703  axunndlem1  8706  axunnd  8707  axpowndlem2  8709  axpowndlem2OLD  8710  axpowndlem3  8711  axpowndlem3OLD  8712  axpowndlem4  8713  axpownd  8714  axregndlem2  8716  axinfndlem1  8718  axinfnd  8719  axacndlem4  8723  axacndlem5  8724  axacnd  8725  gchaleph2  8785  elwina  8799  elina  8800  winaon  8801  inawina  8803  winainf  8807  winalim  8808  tskr1om2  8881  r1tskina  8895  gruina  8931  grur1a  8932  indpi  9022  nqerrel  9047  recidnq  9080  ltaddnq  9089  pncan3  9564  divcan2  9948  ltp1  10113  ltm1  10115  recreclt  10177  elnn0z  10604  nn0ind-raph  10687  faclbnd5  12015  hashfun  12140  2swrd2eqwrdeq  12494  caucvgrlem  13091  fsumcnv  13181  ef01bndlem  13408  sin01gt0  13414  cos01gt0  13415  egt2lt3  13428  cnso  13469  4sqlem12  13957  funcres  14746  fuchom  14811  xpsmnd  15401  mulgfval  15565  xpsgrp  15611  nmznsg  15662  symgplusg  15831  frgp0  16194  gsumval3  16317  pwssplit1  16949  mvrf1  17309  blssioo  20072  dvidlem  21090  dvcj  21124  dvrec  21129  rolle  21162  cmvth  21163  mvth  21164  dvlip  21165  dvlipcn  21166  dv11cn  21173  dvivthlem2  21181  lhop1lem  21185  lhop1  21186  lhop2  21187  q1peqb  21367  pserdv  21635  sinhalfpilem  21666  tangtx  21708  logneg2  21805  lgseisenlem4  22432  dchrisum0lem3  22509  mulogsum  22522  pntrlog2bndlem1  22567  axlowdimlem7  22873  axlowdimlem10  22876  axcontlem6  22894  constr3lem2  23211  hsn0elch  24330  axpjcl  24482  omlsilem  24484  pjchi  24514  shs00i  24532  chj00i  24569  chabs1  24598  pjspansn  24659  chscllem1  24719  osumcor2i  24726  nonbooli  24733  atcvat4i  25480  xppreima  25644  xdivrec  25780  sqsscirc1  26047  1stmbfm  26384  2ndmbfm  26385  eulerpartlemgh  26464  cvmlift3lem5  26915  cvmlift3lem7  26917  fprodcnv  27196  dfon2lem3  27300  dfon2lem7  27304  distel  27319  altopthsn  27694  wl-ax12v2  28081  dvasin  28151  areacirclem4  28158  heiborlem8  28388  0rngo  28498  islssfg2  29097  areaquad  29265  stoweidlem13  29482  stoweidlem26  29495  stoweidlem34  29503  wallispilem4  29537  ccatw2s1p1  29943  el2spthonot0  30064  frisusgranb  30263  extwwlkfablem2  30345  gsumXval3lem1  30463  gsumXval3lem2  30464  gsumXval3  30465  bnj981  31521  bnj1148  31565  bnj1154  31568  bj-axc15v  31771  lshpinN  32071  trlid0  33257  hdmap10lem  34924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator