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

Theorem mpbii 215
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  |-  ps
mpbii.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbii  |-  ( ph  ->  ch )

Proof of Theorem mpbii
StepHypRef Expression
1 mpbii.min . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpbii.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbid 214 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  elimh  968  ax12v2  2177  eqcomd  2459  eqvisset  3055  vtoclgf  3107  vtoclg1f  3108  eueq3  3215  sbc2or  3278  csbiegf  3389  un00  3802  elimhyp  3941  elimhyp2v  3942  elimhyp3v  3943  elimhyp4v  3944  elimdhyp  3946  keephyp2v  3948  keephyp3v  3949  sneqr  4142  preqr1OLD  4152  preq12b  4154  prel12  4155  nfopd  4186  ssex  4550  pwne0  4576  opthwiener  4706  isso2i  4790  nfimad  5180  dfrel2  5289  ordtri3or  5458  on0eqel  5543  funsng  5631  cnvresid  5658  nffvd  5879  fnbrfvb  5910  fvelrnb  5917  fvelimab  5926  funfvop  5999  iunpw  6610  onsucuni  6660  onuninsuci  6672  tposf12  7003  oaword1  7258  oneo  7287  nnaword1  7335  nnneo  7357  inficl  7944  fipwuni  7945  infeq5i  8146  cantnflt  8182  cantnflem1  8199  cnfcom  8210  rankidn  8298  rankr1id  8338  rankxpsuc  8358  iscard  8414  iscard2  8415  carduni  8420  cardmin2  8437  infxpenlem  8449  alephgeom  8518  cardaleph  8525  infenaleph  8527  iscard3  8529  alephsson  8536  alephfp  8544  alephval3  8546  dfac12k  8582  axdc3lem2  8886  alephval2  9002  alephreg  9012  cfpwsdom  9014  alephom  9015  axrepndlem1  9022  axunndlem1  9025  axunnd  9026  axpowndlem2  9028  axpowndlem3  9029  axpowndlem4  9030  axpownd  9031  axregndlem2  9033  axinfndlem1  9035  axinfnd  9036  axacndlem4  9040  axacndlem5  9041  axacnd  9042  gchaleph2  9102  elwina  9116  elina  9117  winaon  9118  inawina  9120  winainf  9124  winalim  9125  tskr1om2  9198  r1tskina  9212  gruina  9248  grur1a  9249  indpi  9337  nqerrel  9362  recidnq  9395  ltaddnq  9404  pncan3  9888  divcan2  10285  ltp1  10450  ltm1  10452  recreclt  10512  elnn0z  10957  nn0ind-raph  11042  fzdifsuc  11862  fsuppmapnn0fiubex  12211  faclbnd5  12490  hashfun  12616  2swrd2eqwrdeq  13040  caucvgrlem  13748  caucvgrlemOLD  13749  fsumcnv  13846  fprodcnv  14049  ef01bndlem  14250  sin01gt0  14256  cos01gt0  14257  egt2lt3  14270  cnso  14311  4sqlem12  14912  funcres  15813  fuchom  15878  xpsmnd  16588  mulgfval  16771  xpsgrp  16817  nmznsg  16873  symgplusg  17042  frgp0  17422  gsumval3lem1  17551  gsumval3lem2  17552  gsumval3  17553  pwssplit1  18294  mvrf1  18661  blssioo  21825  dvidlem  22882  dvcj  22916  dvrec  22921  rolle  22954  cmvth  22955  mvth  22956  dvlip  22957  dvlipcn  22958  dv11cn  22965  dvivthlem2  22973  lhop1lem  22977  lhop1  22978  lhop2  22979  q1peqb  23117  pserdv  23396  sinhalfpilem  23430  tangtx  23472  efabl  23511  logneg2  23576  lgseisenlem4  24292  dchrisum0lem3  24369  mulogsum  24382  pntrlog2bndlem1  24427  axlowdimlem7  24990  axlowdimlem10  24993  axcontlem6  25011  constr3lem2  25386  el2spthonot0  25611  frisusgranb  25737  extwwlkfablem2  25818  hsn0elch  26913  axpjcl  27065  omlsilem  27067  pjchi  27097  shs00i  27115  chj00i  27152  chabs1  27181  pjspansn  27242  chscllem1  27302  osumcor2i  27309  nonbooli  27316  atcvat4i  28062  xppreima  28260  xdivrec  28408  psgndmfi  28621  sqsscirc1  28726  1stmbfm  29094  2ndmbfm  29095  carsgclctunlem2  29163  eulerpartlemgh  29223  bnj1148  29817  bnj1154  29820  cvmlift3lem5  30058  cvmlift3lem7  30060  logi  30382  dfon2lem3  30443  dfon2lem7  30447  distel  30462  altopthsn  30740  bj-elimhyp  31165  bj-axc15v  31374  bj-exlimmpbi  31525  wl-ax12v3  31924  poimirlem9  31961  poimirlem26  31978  poimirlem27  31979  poimirlem32  31984  dvasin  32040  areacirclem4  32047  heiborlem8  32162  0rngo  32272  ax12eq  32524  ax12el  32525  ax12inda  32531  ax12v2-o  32532  lshpinN  32567  trlid0  33754  hdmap10lem  35422  islssfg2  35941  areaquad  36113  rnmptc  37447  fperdvper  37800  itgvol0  37855  stoweidlem13  37883  stoweidlem26  37896  stoweidlem34  37905  wallispilem4  37940  dirkercncflem1  37975  dirkercncflem3  37977  dirkercncflem4  37978  fourierdlem35  38015  fourierdlem73  38053  bgoldbwt  38888  sgoldbalt  38892  nnsum4primeseven  38905  nnsum4primesevenALTV  38906  bgoldbtbndlem1  38910  bgoldbtbndlem3  38912  rusgr1vtxlem  39612
  Copyright terms: Public domain W3C validator