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

Theorem mpbii 223
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 222 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  elimh  1050  axc15  2339  eqcomd  2657  eqvisset  3242  vtoclgf  3295  vtoclg1f  3296  eueq3  3414  sbc2or  3477  csbiegf  3590  un00  4044  elimhyp  4179  elimhyp2v  4180  elimhyp3v  4181  elimhyp4v  4182  elimdhyp  4184  keephyp2v  4186  keephyp3v  4187  preq12b  4413  prel12  4414  nfopd  4450  ssex  4835  opthwiener  5005  isso2i  5096  nfimad  5510  dfrel2  5618  ordtri3or  5793  on0eqel  5883  funsng  5975  cnvresid  6006  nffvd  6238  fnbrfvb  6274  fvelrnb  6282  fvelimab  6292  funfvop  6369  iunpw  7020  onsucuni  7070  onuninsuci  7082  tposf12  7422  oaword1  7677  oneo  7706  nnaword1  7754  nnneo  7776  inficl  8372  fipwuni  8373  infeq5i  8571  cantnflt  8607  cantnflem1  8624  cnfcom  8635  rankidn  8723  rankr1id  8763  rankxpsuc  8783  iscard  8839  iscard2  8840  carduni  8845  cardmin2  8862  infxpenlem  8874  alephgeom  8943  cardaleph  8950  infenaleph  8952  iscard3  8954  alephsson  8961  alephfp  8969  alephval3  8971  dfac12k  9007  axdc3lem2  9311  alephval2  9432  alephreg  9442  cfpwsdom  9444  alephom  9445  axrepndlem1  9452  axunndlem1  9455  axunnd  9456  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axpownd  9461  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  gchaleph2  9532  elwina  9546  elina  9547  winaon  9548  inawina  9550  winainf  9554  winalim  9555  tskr1om2  9628  r1tskina  9642  gruina  9678  grur1a  9679  indpi  9767  nqerrel  9792  recidnq  9825  ltaddnq  9834  pncan3  10327  divcan2  10731  ltp1  10899  ltm1  10901  recreclt  10960  elnn0z  11428  nn0ind-raph  11515  fzdifsuc  12438  2tnp1ge0ge0  12670  fsuppmapnn0fiubex  12832  faclbnd5  13125  hashfun  13262  ccatalpha  13411  2swrd2eqwrdeq  13742  caucvgrlem  14447  fsumcnv  14548  fprodcnv  14757  ef01bndlem  14958  sin01gt0  14964  cos01gt0  14965  egt2lt3  14978  cnso  15020  ltoddhalfle  15132  4sqlem12  15707  funcres  16603  fuchom  16668  xpsmnd  17377  xpsgrp  17581  mulgfval  17589  nmznsg  17685  symgplusg  17855  frgp0  18219  gsumval3lem1  18352  gsumval3lem2  18353  gsumval3  18354  pwssplit1  19107  mvrf1  19473  blssioo  22645  dvidlem  23724  dvcj  23758  dvrec  23763  rolle  23798  cmvth  23799  mvth  23800  dvlip  23801  dvlipcn  23802  dv11cn  23809  dvivthlem2  23817  lhop1lem  23821  lhop1  23822  lhop2  23823  q1peqb  23959  pserdv  24228  sinhalfpilem  24260  tangtx  24302  efabl  24341  logneg2  24406  gausslemma2dlem1a  25135  lgseisenlem4  25148  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  dchrisum0lem3  25253  mulogsum  25266  pntrlog2bndlem1  25311  axlowdimlem7  25873  axlowdimlem10  25876  axcontlem6  25894  umgrbi  26041  rusgr1vtxlem  26539  3wlkond  27149  frcond3  27249  hsn0elch  28233  axpjcl  28387  omlsilem  28389  pjchi  28419  shs00i  28437  chj00i  28474  chabs1  28503  pjspansn  28564  chscllem1  28624  osumcor2i  28631  nonbooli  28638  atcvat4i  29384  xppreima  29577  xdivrec  29763  psgndmfi  29974  sqsscirc1  30082  1stmbfm  30450  2ndmbfm  30451  carsgclctunlem2  30509  eulerpartlemgh  30568  hgt750leme  30864  bnj1148  31190  bnj1154  31193  cvmlift3lem5  31431  cvmlift3lem7  31433  logi  31746  dfon2lem3  31814  dfon2lem7  31818  distel  31833  altopthsn  32193  bj-exlimmpbi  33031  poimirlem9  33548  poimirlem26  33565  poimirlem27  33566  poimirlem32  33571  dvasin  33626  areacirclem4  33633  heiborlem8  33747  0rngo  33956  ax12eq  34545  ax12el  34546  ax12inda  34552  ax12v2-o  34553  nfded  34572  nfded2  34573  nfunidALT2  34574  lshpinN  34594  trlid0  35781  hdmap10lem  37448  islssfg2  37958  areaquad  38119  rnmptc  39667  fperdvper  40451  itgvol0  40502  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  wallispilem4  40603  dirkercncflem1  40638  dirkercncflem3  40640  dirkercncflem4  40641  fourierdlem35  40677  fourierdlem73  40714  lighneallem4b  41851  sbgoldbwt  41990  sbgoldbalt  41994  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  bgoldbtbndlem3  42020
  Copyright terms: Public domain W3C validator