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  947  ax12vOLD  1796  ax12v2  2043  ax12eq  2251  ax12el  2252  ax12inda  2258  ax12v2-o  2259  eqcomd  2462  eqvisset  3089  vtoclgf  3137  vtoclg1f  3138  eueq3  3244  sbc2or  3306  csbiegf  3425  un00  3828  elimhyp  3964  elimhyp2v  3965  elimhyp3v  3966  elimhyp4v  3967  elimdhyp  3969  keephyp2v  3971  keephyp3v  3972  sneqr  4157  preqr1  4163  preq12b  4165  prel12  4166  nfopd  4193  ssex  4553  pwne0  4579  opthwiener  4710  isso2i  4790  ordtri3or  4868  on0eqel  4953  nfimad  5297  dfrel2  5407  funsng  5583  cnvresid  5607  nffvd  5822  fnbrfvb  5855  fvelrnb  5862  fvelimab  5870  funfvop  5938  iunpw  6523  onsucuni  6572  onuninsuci  6584  tposf12  6904  oaword1  7125  oneo  7154  nnaword1  7202  nnneo  7224  inficl  7811  fipwuni  7812  infeq5i  7979  cantnflt  8017  cantnflem1  8034  cantnfltOLD  8047  cantnflem1OLD  8057  cnfcom  8070  cnfcomOLD  8078  rankidn  8166  rankr1id  8206  rankxpsuc  8226  iscard  8282  iscard2  8283  carduni  8288  cardmin2  8305  infxpenlem  8317  alephgeom  8389  cardaleph  8396  infenaleph  8398  iscard3  8400  alephsson  8407  alephfp  8415  alephval3  8417  dfac12k  8453  axdc3lem2  8757  alephval2  8873  alephreg  8883  cfpwsdom  8885  alephom  8886  axrepndlem1  8893  axunndlem1  8896  axunnd  8897  axpowndlem2  8899  axpowndlem2OLD  8900  axpowndlem3  8901  axpowndlem3OLD  8902  axpowndlem4  8903  axpownd  8904  axregndlem2  8906  axinfndlem1  8909  axinfnd  8910  axacndlem4  8914  axacndlem5  8915  axacnd  8916  gchaleph2  8976  elwina  8990  elina  8991  winaon  8992  inawina  8994  winainf  8998  winalim  8999  tskr1om2  9072  r1tskina  9086  gruina  9122  grur1a  9123  indpi  9213  nqerrel  9238  recidnq  9271  ltaddnq  9280  pncan3  9755  divcan2  10139  ltp1  10304  ltm1  10306  recreclt  10368  elnn0z  10797  nn0ind-raph  10880  fzdifsuc  11661  fsuppmapnn0fiubex  11955  faclbnd5  12231  hashfun  12357  2swrd2eqwrdeq  12711  caucvgrlem  13308  fsumcnv  13398  ef01bndlem  13626  sin01gt0  13632  cos01gt0  13633  egt2lt3  13646  cnso  13687  4sqlem12  14175  funcres  14965  fuchom  15030  xpsmnd  15620  mulgfval  15787  xpsgrp  15833  nmznsg  15884  symgplusg  16053  frgp0  16418  gsumval3OLD  16543  gsumval3lem1  16544  gsumval3lem2  16545  gsumval3  16546  pwssplit1  17316  mvrf1  17675  blssioo  20771  dvidlem  21790  dvcj  21824  dvrec  21829  rolle  21862  cmvth  21863  mvth  21864  dvlip  21865  dvlipcn  21866  dv11cn  21873  dvivthlem2  21881  lhop1lem  21885  lhop1  21886  lhop2  21887  q1peqb  22026  pserdv  22294  sinhalfpilem  22325  tangtx  22367  logneg2  22464  lgseisenlem4  23091  dchrisum0lem3  23168  mulogsum  23181  pntrlog2bndlem1  23226  axlowdimlem7  23663  axlowdimlem10  23666  axcontlem6  23684  constr3lem2  24001  hsn0elch  25120  axpjcl  25272  omlsilem  25274  pjchi  25304  shs00i  25322  chj00i  25359  chabs1  25388  pjspansn  25449  chscllem1  25509  osumcor2i  25516  nonbooli  25523  atcvat4i  26270  xppreima  26431  xdivrec  26563  sqsscirc1  26795  1stmbfm  27131  2ndmbfm  27132  eulerpartlemgh  27217  cvmlift3lem5  27668  cvmlift3lem7  27670  fprodcnv  27950  dfon2lem3  28054  dfon2lem7  28058  distel  28073  altopthsn  28448  dvasin  28940  areacirclem4  28947  heiborlem8  29177  0rngo  29287  islssfg2  29884  areaquad  30052  stoweidlem13  30542  stoweidlem26  30555  stoweidlem34  30563  wallispilem4  30597  ccatw2s1p1  31146  el2spthonot0  31267  frisusgranb  31466  extwwlkfablem2  31548  bnj981  32786  bnj1148  32830  bnj1154  32833  bj-elimhyp  32939  bj-axc15v  33110  bj-exlimmpbi  33258  lshpinN  33485  trlid0  34671  hdmap10lem  36338
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