ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbid Unicode version

Theorem mpbid 135
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbid.min  |-  ( ph  ->  ps )
mpbid.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbid  |-  ( ph  ->  ch )

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2  |-  ( ph  ->  ps )
2 mpbid.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 132 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbii  136  annimdc  845  mpbi2and  850  bilukdc  1287  equs5or  1711  eqtrd  2072  eleqtrd  2116  neeqtrd  2233  3netr3d  2237  rexlimd2  2431  ceqsalt  2580  vtoclgft  2604  vtoclegft  2625  elrab3t  2697  eueq2dc  2714  sbceq1dd  2770  csbiedf  2887  sseqtrd  2981  3sstr3d  2987  snssd  3509  dfnfc2  3598  breqtrd  3788  3brtr3d  3793  csbexga  3885  reuhypd  4203  reg2exmidlema  4259  elirr  4266  en2lp  4278  onsucuni2  4288  finds  4323  iota4  4885  iota4an  4886  funimaexglem  4982  fneu  5003  fco2  5057  fssres2  5067  fresin  5068  feu  5072  f1orescnv  5142  resdif  5148  funcocnv2  5151  f1oprg  5168  fvelrnb  5221  fimacnv  5296  f1oresrab  5329  fsn2  5337  xpsng  5338  fnressn  5349  fsnunf  5362  foeqcnvco  5430  isores1  5454  isoini2  5458  riota5f  5492  riotass2  5494  riotass  5495  ovmpt2dxf  5626  elopabi  5821  cnvf1o  5846  smores3  5908  tfrlemisucaccv  5939  nnsucsssuc  6071  erref  6126  iserd  6132  swoer  6134  swoord1  6135  swoord2  6136  erth  6150  erthi  6152  eroveu  6197  fndmeng  6289  phplem4  6318  phplem4on  6329  fidifsnen  6331  dif1en  6337  fisbth  6340  diffisn  6350  ac6sfi  6352  ordiso2  6357  dfplpq2  6452  ltanqi  6500  ltmnqi  6501  ltaddnq  6505  subhalfnqq  6512  ltbtwnnqq  6513  archnqq  6515  prarloclemarch2  6517  enq0sym  6530  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nnnq0lem1  6544  distrnq0  6557  prarloclemlt  6591  prarloclemn  6597  prarloclemcalc  6600  genplt2i  6608  addnqprllem  6625  addnqprulem  6626  addlocprlemgt  6632  appdivnq  6661  prmuloc2  6665  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemru  6710  prplnqu  6718  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemladdfu  6752  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  archrecnq  6761  archrecpr  6762  caucvgprlemk  6763  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprprlemk  6781  caucvgprprlemnkeqj  6788  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlem1  6807  caucvgprprlem2  6808  prsrlem1  6827  addgt0sr  6860  srpospr  6867  prsrriota  6872  caucvgsrlemgt1  6879  caucvgsrlemoffgt1  6883  caucvgsr  6886  recriota  6964  lelttr  7106  ltletr  7107  ltnsymd  7136  cnegexlem3  7188  cnegex2  7190  addcanad  7197  addcan2ad  7198  negcon1ad  7317  negne0d  7320  negrebd  7321  subeq0d  7330  subne0ad  7333  neg11d  7334  subcand  7363  subcan2d  7364  ltadd2  7416  ltadd2dd  7419  add20  7469  ltnegcon1d  7516  ltnegcon2d  7517  lenegcon1d  7518  lenegcon2d  7519  subled  7539  lesubd  7540  ltsub23d  7541  ltsub13d  7542  ltadd1dd  7547  ltsub1dd  7548  ltsub2dd  7549  leadd1dd  7550  leadd2dd  7551  lesub1dd  7552  lesub2dd  7553  recexre  7569  apreap  7578  ltmul1a  7582  reapmul1  7586  cru  7593  apreim  7594  mulge0  7610  leltap  7615  ltleap  7621  ltapd  7627  ap0gt0  7629  ap0gt0d  7630  subap0d  7631  mulcanapad  7644  mulcanap2ad  7645  eqnegad  7710  diveqap0d  7772  diveqap1d  7773  divap1d  7776  rec11apd  7786  div11apd  7805  recgt0  7816  prodgt0  7818  lemul1a  7824  lemulge12  7833  lt2msq1  7851  lediv12a  7860  recreclt  7866  nn1suc  7933  nnnlt1  7940  nn2ge  7946  nn1gt1  7947  nnrecl  8179  nn0nlt0  8208  elnn0z  8258  elz2  8312  nn0n0n1ge2b  8320  nnm1ge0  8326  nn0ge0div  8327  zextle  8331  nn0ind-raph  8355  zindd  8356  uzneg  8491  eluzadd  8501  eluzsub  8502  uzm1  8503  uz3m2nn  8515  nn01to3  8552  ltrec1d  8643  lerec2d  8644  ledivdivd  8648  divge1  8649  ltmul1dd  8678  ltmul2dd  8679  ltdiv1dd  8680  lediv1dd  8681  ltdiv23d  8683  lediv23d  8684  xrlelttr  8722  xrltletr  8723  ixxdisj  8772  icoshftf1o  8859  icodisj  8860  lincmb01cmp  8871  iccf1o  8872  uzsubsubfz  8911  fzdisj  8916  fzopth  8924  fznatpl1  8938  fzsuc2  8941  fzp1disj  8942  fzrev2i  8948  uzdisj  8955  fseq1p1m1  8956  fzm1  8962  fzneuz  8963  fzp1nel  8966  fzrevral  8967  elfz0addOLD  8980  fznn0sub2  8985  fz0fzdiffz0  8987  difelfzle  8992  difelfznle  8993  nn0disj  8995  fzonnsub  9025  fzodisj  9034  fzouzdisj  9036  eluzgtdifelfzo  9053  ubmelfzo  9056  fzonn0p1p1  9069  ubmelm1fzo  9082  fzostep1  9093  subfzo0  9097  qtri3or  9098  qbtwnzlemex  9105  rebtwn2z  9109  qbtwnrelemcalc  9110  qbtwnre  9111  flid  9126  flqwordi  9130  flqmulnn0  9141  flhalf  9144  flltdivnn0lt  9146  fldiv4p1lem1div2  9147  intfracq  9162  flqdiv  9163  flqpmodeq  9169  modqmulnn  9184  monoord2  9236  isermono  9237  serile  9253  expival  9257  expnegap0  9263  expgt1  9293  ltexp2a  9306  le2sq2  9329  nnlesq  9356  bernneq  9369  expnbnd  9372  expnlbnd  9373  expnlbnd2  9374  expeq0d  9377  sq11d  9413  cjth  9446  cjdivap  9509  cjne0d  9547  cjap0d  9548  cvg1nlemcxze  9581  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemover  9608  resqrexlemdecn  9610  resqrexlemlo  9611  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621  leabs  9672  absrele  9679  nn0abscl  9681  ltabs  9683  abslt  9684  absle  9685  abstri  9700  amgm2  9714  sqr11d  9769  abs00d  9782  climi  9808  climge0  9845  climle  9854  climserile  9865  climrecvg1n  9867
  Copyright terms: Public domain W3C validator