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

Theorem mpbii 211
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-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 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  elimh  956  ax12vOLD  1856  ax12v2  2083  ax12eq  2271  ax12el  2272  ax12inda  2278  ax12v2-o  2279  eqcomd  2465  eqvisset  3117  vtoclgf  3165  vtoclg1f  3166  eueq3  3274  sbc2or  3336  csbiegf  3458  un00  3862  elimhyp  4000  elimhyp2v  4001  elimhyp3v  4002  elimhyp4v  4003  elimdhyp  4005  keephyp2v  4007  keephyp3v  4008  sneqr  4197  preqr1  4204  preq12b  4206  prel12  4207  nfopd  4234  ssex  4596  pwne0  4622  opthwiener  4754  isso2i  4837  ordtri3or  4915  on0eqel  5000  nfimad  5351  dfrel2  5462  funsng  5639  cnvresid  5663  nffvd  5880  fnbrfvb  5913  fvelrnb  5920  fvelimab  5929  funfvop  5999  iunpw  6614  onsucuni  6663  onuninsuci  6675  tposf12  6999  oaword1  7220  oneo  7249  nnaword1  7297  nnneo  7319  inficl  7905  fipwuni  7906  infeq5i  8074  cantnflt  8112  cantnflem1  8129  cantnfltOLD  8142  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  rankidn  8261  rankr1id  8301  rankxpsuc  8321  iscard  8377  iscard2  8378  carduni  8383  cardmin2  8400  infxpenlem  8412  alephgeom  8484  cardaleph  8491  infenaleph  8493  iscard3  8495  alephsson  8502  alephfp  8510  alephval3  8512  dfac12k  8548  axdc3lem2  8852  alephval2  8968  alephreg  8978  cfpwsdom  8980  alephom  8981  axrepndlem1  8988  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  gchaleph2  9071  elwina  9085  elina  9086  winaon  9087  inawina  9089  winainf  9093  winalim  9094  tskr1om2  9167  r1tskina  9181  gruina  9217  grur1a  9218  indpi  9306  nqerrel  9331  recidnq  9364  ltaddnq  9373  pncan3  9851  divcan2  10240  ltp1  10405  ltm1  10407  recreclt  10469  elnn0z  10902  nn0ind-raph  10989  fzdifsuc  11768  fsuppmapnn0fiubex  12098  faclbnd5  12376  hashfun  12495  ccatw2s1p1  12640  2swrd2eqwrdeq  12891  caucvgrlem  13495  fsumcnv  13588  fprodcnv  13787  ef01bndlem  13919  sin01gt0  13925  cos01gt0  13926  egt2lt3  13939  cnso  13980  4sqlem12  14474  funcres  15265  fuchom  15330  xpsmnd  15960  mulgfval  16143  xpsgrp  16189  nmznsg  16245  symgplusg  16414  frgp0  16778  gsumval3OLD  16908  gsumval3lem1  16909  gsumval3lem2  16910  gsumval3  16911  pwssplit1  17705  mvrf1  18081  blssioo  21300  dvidlem  22319  dvcj  22353  dvrec  22358  rolle  22391  cmvth  22392  mvth  22393  dvlip  22394  dvlipcn  22395  dv11cn  22402  dvivthlem2  22410  lhop1lem  22414  lhop1  22415  lhop2  22416  q1peqb  22555  pserdv  22824  sinhalfpilem  22856  tangtx  22898  efabl  22937  logneg2  23000  lgseisenlem4  23627  dchrisum0lem3  23704  mulogsum  23717  pntrlog2bndlem1  23762  axlowdimlem7  24251  axlowdimlem10  24254  axcontlem6  24272  constr3lem2  24646  el2spthonot0  24871  frisusgranb  24997  extwwlkfablem2  25078  hsn0elch  26166  axpjcl  26318  omlsilem  26320  pjchi  26350  shs00i  26368  chj00i  26405  chabs1  26434  pjspansn  26495  chscllem1  26555  osumcor2i  26562  nonbooli  26569  atcvat4i  27316  xppreima  27487  xdivrec  27623  sqsscirc1  27890  1stmbfm  28231  2ndmbfm  28232  eulerpartlemgh  28317  cvmlift3lem5  28768  cvmlift3lem7  28770  logi  29121  dfon2lem3  29217  dfon2lem7  29221  distel  29236  altopthsn  29611  dvasin  30103  areacirclem4  30110  heiborlem8  30314  0rngo  30424  islssfg2  31017  areaquad  31184  rnmptc  31449  fperdvper  31715  itgvol0  31767  stoweidlem13  31795  stoweidlem26  31808  stoweidlem34  31816  wallispilem4  31850  dirkercncflem1  31885  dirkercncflem3  31887  dirkercncflem4  31888  fourierdlem35  31924  fourierdlem73  31962  bnj1148  34052  bnj1154  34055  bj-elimhyp  34160  bj-axc15v  34330  bj-exlimmpbi  34478  lshpinN  34714  trlid0  35901  hdmap10lem  37569
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 185
  Copyright terms: Public domain W3C validator