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

Theorem mpbii 236
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 235 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  dedt  1081  eqcomd  2830  nfabdw  3003  eqvisset  3497  vtocl  3545  vtoclgf  3551  vtoclg1f  3552  vtoclg  3553  eueq3  3688  sbc2or  3767  csbiegf  3899  un00  4377  elimhyp  4513  elimhyp2v  4514  elimhyp3v  4515  elimhyp4v  4516  elimdhyp  4518  keephyp2v  4520  keephyp3v  4521  preq12b  4765  nfopd  4806  ssex  5211  opthwiener  5391  isso2i  5495  nfimad  5925  dfrel2  6033  ordtri3or  6210  on0eqel  6295  funsng  6393  cnvresid  6421  nffvd  6673  fnbrfvb  6709  fvelrnb  6717  fvelimab  6728  funfvop  6811  fvsnun2  6936  rnmptcOLD  6961  iunpw  7487  onsucuni  7537  onuninsuci  7549  tposf12  7913  oaword1  8174  oneo  8203  nnaword1  8251  nnneo  8274  inficl  8886  fipwuni  8887  infeq5i  9096  cantnflt  9132  cantnflem1  9149  cnfcom  9160  rankidn  9248  rankr1id  9288  rankxpsuc  9308  iscard  9401  iscard2  9402  carduni  9407  cardmin2  9425  infxpenlem  9437  alephgeom  9506  cardaleph  9513  infenaleph  9515  iscard3  9517  alephsson  9524  alephfp  9532  alephval3  9534  dfac12k  9571  axdc3lem2  9871  alephval2  9992  alephreg  10002  cfpwsdom  10004  alephom  10005  axrepndlem1  10012  axunndlem1  10015  axunnd  10016  axpowndlem2  10018  axpowndlem3  10019  axpowndlem4  10020  axpownd  10021  axregndlem2  10023  axinfndlem1  10025  axinfnd  10026  axacndlem4  10030  axacndlem5  10031  axacnd  10032  gchaleph2  10092  elwina  10106  elina  10107  winaon  10108  inawina  10110  winainf  10114  winalim  10115  tskr1om2  10188  r1tskina  10202  gruina  10238  grur1a  10239  indpi  10327  nqerrel  10352  recidnq  10385  ltaddnq  10394  pncan3  10892  divcan2  11304  ltp1  11478  ltm1  11480  recreclt  11537  elnn0z  11991  nn0ind-raph  12079  fzdifsuc  12971  2tnp1ge0ge0  13203  fsuppmapnn0fiubex  13364  faclbnd5  13663  hashfun  13803  ccatalpha  13947  caucvgrlem  15029  fsumcnv  15128  fprodcnv  15337  ef01bndlem  15537  sin01gt0  15543  cos01gt0  15544  egt2lt3  15559  cnso  15600  ltoddhalfle  15710  4sqlem12  16290  funcres  17166  fuchom  17231  xpsmnd  17951  xpsgrp  18218  mulgfval  18226  mulgfvalALT  18227  nmznsg  18320  frgp0  18886  gsumval3lem2  19026  gsumval3  19027  pwssplit1  19831  mvrf1  20670  blssioo  23407  dvidlem  24525  dvcj  24560  dvrec  24565  rolle  24600  cmvth  24601  mvth  24602  dvlip  24603  dvlipcn  24604  dv11cn  24611  dvivthlem2  24619  lhop1lem  24623  lhop1  24624  lhop2  24625  q1peqb  24762  pserdv  25031  sinhalfpilem  25063  tangtx  25105  efabl  25149  logneg2  25213  gausslemma2dlem1a  25956  lgseisenlem4  25969  2lgslem3a  25987  2lgslem3b  25988  2lgslem3c  25989  2lgslem3d  25990  dchrisum0lem3  26110  mulogsum  26123  pntrlog2bndlem1  26168  axlowdimlem7  26749  axlowdimlem10  26752  axcontlem6  26770  umgrbi  26901  rusgr1vtxlem  27384  clwwlknonwwlknonb  27898  3wlkond  27963  frcond3  28061  hsn0elch  29038  axpjcl  29190  omlsilem  29192  pjchi  29222  shs00i  29240  chj00i  29277  chabs1  29306  pjspansn  29367  chscllem1  29427  osumcor2i  29434  nonbooli  29441  atcvat4i  30187  xppreima  30409  xdivrec  30618  wrdt2ind  30642  psgndmfi  30776  sqsscirc1  31212  1stmbfm  31579  2ndmbfm  31580  carsgclctunlem2  31638  eulerpartlemgh  31697  hgt750leme  31990  bnj1148  32329  bnj1154  32332  cvmlift3lem5  32631  cvmlift3lem7  32633  logi  33027  dfon2lem3  33091  dfon2lem7  33095  distel  33109  altopthsn  33483  bj-ax12  34051  bj-exlimmpbi  34301  irrdiff  34689  rdgssun  34744  poimirlem9  35015  poimirlem26  35032  poimirlem27  35033  poimirlem32  35038  dvasin  35090  areacirclem4  35097  heiborlem8  35205  0rngo  35414  ax12eq  36186  ax12el  36187  ax12inda  36193  ax12v2-o  36194  nfded  36212  nfded2  36213  nfunidALT2  36214  lshpinN  36234  trlid0  37421  hdmap10lem  39084  lcmineqlem  39292  metakunt24  39323  renegid  39446  repncan3  39456  sn-00idlem2  39472  reixi  39494  sn-ltp1  39513  islssfg2  39936  areaquad  40087  fperdvper  42492  itgvol0  42541  stoweidlem13  42586  stoweidlem26  42599  stoweidlem34  42607  wallispilem4  42641  dirkercncflem1  42676  dirkercncflem3  42678  dirkercncflem4  42679  fourierdlem35  42715  fourierdlem73  42752  funressndmafv2rn  43710  dfatbrafv2b  43732  fnbrafv2b  43735  ichnfimlem  43911  lighneallem4b  44058  sbgoldbwt  44226  sbgoldbalt  44230  nnsum4primeseven  44249  nnsum4primesevenALTV  44250  bgoldbtbndlem1  44254  bgoldbtbndlem3  44256
  Copyright terms: Public domain W3C validator