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

Theorem mpbid 145
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 142 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbii  146  annimdc  881  mpbi2and  887  bilukdc  1330  equs5or  1755  eqtrd  2117  eleqtrd  2163  neeqtrd  2279  3netr3d  2283  rexlimd2  2483  ceqsalt  2639  vtoclgft  2663  vtoclegft  2684  elrab3t  2761  eueq2dc  2779  sbceq1dd  2835  csbiedf  2957  sseqtrd  3051  3sstr3d  3057  ifbothdadc  3408  snssd  3565  dfnfc2  3654  breqtrd  3844  3brtr3d  3849  csbexga  3942  reuhypd  4267  reg2exmidlema  4323  elirr  4330  en2lp  4343  onsucuni2  4353  finds  4388  iota4  4964  iota4an  4965  funimaexglem  5062  fneu  5083  fco2  5141  fssres2  5151  fresin  5152  feu  5156  f1orescnv  5232  resdif  5238  funcocnv2  5241  f1oprg  5258  fvelrnb  5315  fimacnv  5391  f1oresrab  5426  fsn2  5434  xpsng  5435  fnressn  5446  fsnunf  5459  foeqcnvco  5530  isores1  5554  isoini2  5559  riota5f  5593  riotass2  5595  riotass  5596  ovmpt2dxf  5727  elopabi  5922  cnvf1o  5947  smores3  6012  tfrlemisucaccv  6044  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  rdgon  6105  frecabcl  6118  frecsuclem  6125  nnsucsssuc  6207  nnsucuniel  6210  erref  6264  iserd  6270  swoer  6272  swoord1  6273  swoord2  6274  erth  6288  erthi  6290  eroveu  6335  pmresg  6385  mapsn  6399  fndmeng  6479  xpen  6513  phplem4  6523  phplem4on  6535  fidifsnen  6538  dif1en  6547  dif1enen  6548  fisbth  6551  diffisn  6561  ac6sfi  6566  fimax2gtri  6569  en2eqpr  6575  unsnfidcex  6582  unsnfidcel  6583  eqsupti  6635  supisoti  6649  ordiso2  6672  djur  6701  casef  6723  enomnilem  6738  exmidomni  6742  fodjuomnilemm  6745  fodjuomnilemres  6747  dfplpq2  6857  ltanqi  6905  ltmnqi  6906  ltaddnq  6910  subhalfnqq  6917  ltbtwnnqq  6918  archnqq  6920  prarloclemarch2  6922  enq0sym  6935  enq0ref  6936  enq0tr  6937  nqnq0pi  6941  nnnq0lem1  6949  distrnq0  6962  prarloclemlt  6996  prarloclemn  7002  prarloclemcalc  7005  genplt2i  7013  addnqprllem  7030  addnqprulem  7031  addlocprlemgt  7037  appdivnq  7066  prmuloc2  7070  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemru  7115  prplnqu  7123  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemladdfu  7157  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  archrecnq  7166  archrecpr  7167  caucvgprlemk  7168  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprprlemk  7186  caucvgprprlemnkeqj  7193  caucvgprprlemnbj  7196  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlem1  7212  caucvgprprlem2  7213  prsrlem1  7232  addgt0sr  7265  srpospr  7272  prsrriota  7277  caucvgsrlemgt1  7284  caucvgsrlemoffgt1  7288  caucvgsr  7291  recriota  7369  lelttr  7517  ltletr  7518  ltnsymd  7547  lensymd  7549  cnegexlem3  7603  cnegex2  7605  addcanad  7612  addcan2ad  7613  negcon1ad  7732  negne0d  7735  negrebd  7736  subeq0d  7745  subne0ad  7748  neg11d  7749  subcand  7778  subcan2d  7779  ltadd2  7841  ltadd2dd  7844  add20  7896  ltnegcon1d  7943  ltnegcon2d  7944  lenegcon1d  7945  lenegcon2d  7946  subled  7966  lesubd  7967  ltsub23d  7968  ltsub13d  7969  ltadd1dd  7974  ltsub1dd  7975  ltsub2dd  7976  leadd1dd  7977  leadd2dd  7978  lesub1dd  7979  lesub2dd  7980  recexre  7996  apreap  8005  ltmul1a  8009  reapmul1  8013  cru  8020  apreim  8021  mulge0  8037  leltap  8042  ltleap  8048  ltapd  8054  ap0gt0  8056  ap0gt0d  8057  subap0d  8058  mulcanapad  8071  mulcanap2ad  8072  eqnegad  8140  diveqap0d  8202  diveqap1d  8203  divap1d  8206  rec11apd  8216  div11apd  8235  recgt0  8246  prodgt0  8248  lemul1a  8254  lemulge12  8263  lt2msq1  8281  lediv12a  8290  recreclt  8296  nn1suc  8376  nnnlt1  8383  nn2ge  8389  nn1gt1  8390  nnrecl  8604  nn0nlt0  8632  elnn0z  8696  elz2  8751  nn0n0n1ge2b  8759  nnm1ge0  8765  nn0ge0div  8766  zextle  8770  suprzclex  8777  nn0ind-raph  8796  zindd  8797  uzneg  8969  eluzadd  8979  eluzsub  8980  uzm1  8981  uz3m2nn  8993  supminfex  9017  nn01to3  9034  ltrec1d  9126  lerec2d  9127  ledivdivd  9131  divge1  9132  ltmul1dd  9161  ltmul2dd  9162  ltdiv1dd  9163  lediv1dd  9164  ltdiv23d  9166  lediv23d  9167  nn0ledivnn  9170  addlelt  9171  xrlelttr  9203  xrltletr  9204  ixxdisj  9253  icoshftf1o  9340  icodisj  9341  lincmb01cmp  9352  iccf1o  9353  uzsubsubfz  9393  fzdisj  9398  fzopth  9406  fznatpl1  9420  fzsuc2  9423  fzp1disj  9424  fzrev2i  9430  uzdisj  9437  fseq1p1m1  9438  fzm1  9444  fzneuz  9445  fzp1nel  9448  fzrevral  9449  fznn0sub2  9467  fz0fzdiffz0  9469  difelfzle  9473  difelfznle  9474  nn0disj  9477  fzonnsub  9508  fzodisj  9517  fzouzdisj  9519  eluzgtdifelfzo  9536  ubmelfzo  9539  fzonn0p1p1  9552  ubmelm1fzo  9565  fzostep1  9576  exfzdc  9579  subfzo0  9581  qtri3or  9582  exbtwnzlemex  9589  rebtwn2z  9594  qbtwnrelemcalc  9595  qbtwnre  9596  qavgle  9598  apbtwnz  9609  flid  9619  flqwordi  9623  flqmulnn0  9634  flhalf  9637  flltdivnn0lt  9639  fldiv4p1lem1div2  9640  intfracq  9655  flqdiv  9656  flqpmodeq  9662  modqmulnn  9677  mulqaddmodid  9699  modqmuladdim  9702  modqmuladdnn0  9703  m1modge3gt1  9706  q2submod  9720  modaddmodup  9722  modqsubdir  9728  modqeqmodmin  9729  modfzo0difsn  9730  uzsinds  9776  monoord2  9810  isermono  9811  iseqf1olemqcl  9819  iseqf1olemnab  9821  iseqf1olemab  9822  iseqf1olemqf1o  9826  iseqf1olemqk  9827  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1olemp  9835  serile  9851  expival  9855  expnegap0  9861  expgt1  9891  ltexp2a  9905  le2sq2  9928  nnlesq  9955  bernneq  9970  expnbnd  9973  expnlbnd  9974  expnlbnd2  9975  expeq0d  9978  sq11d  10015  expcand  10022  nn0opthd  10026  facdiv  10042  faclbnd6  10048  facubnd  10049  facavg  10050  bcval4  10056  bcp1nk  10066  ibcval5  10067  bcpasc  10070  hashennnuni  10083  focdmex  10091  isfinite4im  10097  hashnncl  10100  hashunlem  10108  fiprsshashgt1  10121  hashfzp1  10128  zfz1isolemiso  10140  iseqcoll  10143  cjth  10175  cjdivap  10238  cjne0d  10276  cjap0d  10277  cvg1nlemcxze  10310  cvg1nlemcau  10312  cvg1nlemres  10313  recvguniq  10323  resqrexlemover  10338  resqrexlemdecn  10340  resqrexlemlo  10341  resqrexlemcalc2  10343  resqrexlemcalc3  10344  resqrexlemnmsq  10345  resqrexlemnm  10346  resqrexlemcvg  10347  resqrexlemglsq  10350  resqrexlemga  10351  leabs  10402  absrele  10411  nn0abscl  10413  ltabs  10415  abslt  10416  absle  10417  abstri  10432  amgm2  10446  sqr11d  10501  abs00d  10514  maxabsle  10532  maxabslemlub  10535  maxleastlt  10543  maxltsup  10546  minmax  10554  climi  10568  climge0  10605  climle  10614  climserile  10625  climrecvg1n  10627  fz1f1o  10654  isummolem3  10659  isummolem2a  10660  isummo  10662  fisumss  10670  zdvdsdc  10692  dvdstr  10708  dvdsadd2b  10718  dvdslelemd  10719  divconjdvds  10725  alzdvds  10730  dvdsext  10731  fzm1ndvds  10732  fzo0dvdseq  10733  zeo3  10743  even2n  10749  mod2eq1n2dvds  10754  nn0ehalf  10778  nnehalf  10779  nno  10781  nn0oddm1d2  10784  divalglemnqt  10795  divalglemex  10797  divalglemeuneg  10798  divalg2  10801  divalgmod  10802  flodddiv4t2lthalf  10812  zsupcllemstep  10816  infssuzex  10820  dvdsbnd  10823  gcdsupex  10824  gcdsupcl  10825  gcddvds  10830  divgcdz  10838  divgcdnn  10841  gcd0id  10845  gcdneg  10848  gcd1  10853  bezoutlemnewy  10860  bezoutlemstep  10861  bezoutlemmo  10870  bezoutlemsup  10873  dfgcd3  10874  bezout  10875  dfgcd2  10878  mulgcd  10880  sqgcd  10893  dvdssqlem  10894  bezoutr1  10897  lcmval  10920  lcmcllem  10924  dvdslcm  10926  lcmgcdlem  10934  lcmdvds  10936  lcmgcdeq  10940  ncoprmgcdne1b  10946  mulgcddvds  10951  rpmulgcd2  10952  qredeu  10954  rpdvds  10956  prmind2  10977  nprm  10980  dvdsnprmd  10982  divgcdodd  10997  isprm6  11001  prmexpb  11005  pw2dvds  11019  pw2dvdseulemle  11020  oddpwdclemdc  11026  sqne2sq  11030  znege1  11031  sqrt2irraplemnn  11032  divnumden  11049  divdenle  11050  qden1elz  11058  nn0sqrtelqelz  11059  hashdvds  11072  crth  11075  phimullem  11076  hashgcdlem  11078  oddennn  11080  nnsf  11333  peano4nninf  11334  nninfalllemn  11336  nninfsellemeq  11344
  Copyright terms: Public domain W3C validator