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

Theorem mpbid 146
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 143 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbii  147  annimdc  906  mpbi2and  912  bilukdc  1359  equs5or  1786  eqtrd  2150  eleqtrd  2196  neeqtrd  2313  3netr3d  2317  rexlimd2  2524  ceqsalt  2686  vtoclgft  2710  vtoclegft  2732  elrab3t  2812  eueq2dc  2830  sbceq1dd  2888  csbiedf  3010  sseqtrd  3105  3sstr3d  3111  ifbothdadc  3473  snssd  3635  dfnfc2  3724  breqdi  3914  breqtrd  3924  3brtr3d  3929  csbexga  4026  reuhypd  4362  reg2exmidlema  4419  elirr  4426  en2lp  4439  onsucuni2  4449  finds  4484  iota4  5076  iota4an  5077  funimaexglem  5176  fneu  5197  fco2  5259  fssres2  5270  fresin  5271  feu  5275  f1orescnv  5351  resdif  5357  funcocnv2  5360  f1oprg  5379  fvelrnb  5437  fimacnv  5517  f1oresrab  5553  fsn2  5562  xpsng  5563  fnressn  5574  fsnunf  5588  foeqcnvco  5659  isores1  5683  isoini2  5688  riota5f  5722  riotass2  5724  riotass  5725  ovmpodxf  5864  elopabi  6061  cnvf1o  6090  smores3  6158  tfrlemisucaccv  6190  tfr1onlemsucaccv  6206  tfrcllemsucaccv  6219  rdgon  6251  frecabcl  6264  frecsuclem  6271  nnsucsssuc  6356  nnsucuniel  6359  erref  6417  iserd  6423  swoer  6425  swoord1  6426  swoord2  6427  erth  6441  erthi  6443  eroveu  6488  pmresg  6538  mapsn  6552  fndmeng  6672  xpen  6707  phplem4  6717  phplem4on  6729  fidifsnen  6732  dif1en  6741  dif1enen  6742  fisbth  6745  diffisn  6755  ac6sfi  6760  fimax2gtri  6763  en2eqpr  6769  unsnfidcex  6776  unsnfidcel  6777  fiintim  6785  fidcenumlemrks  6809  elfi2  6828  elfir  6829  fiuni  6834  fifo  6836  eqsupti  6851  supisoti  6865  ordiso2  6888  casef  6941  difinfsnlem  6952  ctmlemr  6961  ctssdccl  6964  enumct  6968  enomnilem  6978  exmidomni  6982  fodjum  6986  fodjuomnilemres  6988  mkvprop  7000  acfun  7031  ccfunen  7047  dfplpq2  7130  ltanqi  7178  ltmnqi  7179  ltaddnq  7183  subhalfnqq  7190  ltbtwnnqq  7191  archnqq  7193  prarloclemarch2  7195  enq0sym  7208  enq0ref  7209  enq0tr  7210  nqnq0pi  7214  nnnq0lem1  7222  distrnq0  7235  prarloclemlt  7269  prarloclemn  7275  prarloclemcalc  7278  genplt2i  7286  addnqprllem  7303  addnqprulem  7304  addlocprlemgt  7310  appdivnq  7339  prmuloc2  7343  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemru  7388  prplnqu  7396  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemladdfu  7430  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  archrecnq  7439  archrecpr  7440  caucvgprlemk  7441  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprprlemk  7459  caucvgprprlemnkeqj  7466  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemmu  7471  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemopu  7475  caucvgprprlemexbt  7482  caucvgprprlemexb  7483  caucvgprprlem1  7485  caucvgprprlem2  7486  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  suplocexprlemlub  7500  prsrlem1  7518  addgt0sr  7551  srpospr  7559  prsrriota  7564  caucvgsrlemgt1  7571  caucvgsrlemoffgt1  7575  caucvgsr  7578  mappsrprg  7580  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  recriota  7666  axsuploc  7805  lelttr  7820  ltletr  7821  ltnsymd  7850  lensymd  7852  cnegexlem3  7907  cnegex2  7909  addcanad  7916  addcan2ad  7917  negcon1ad  8036  negne0d  8039  negrebd  8040  subeq0d  8049  subne0ad  8052  neg11d  8053  subcand  8082  subcan2d  8083  ltadd2  8149  ltadd2dd  8152  add20  8204  ltnegcon1d  8254  ltnegcon2d  8255  lenegcon1d  8256  lenegcon2d  8257  subled  8277  lesubd  8278  ltsub23d  8279  ltsub13d  8280  ltadd1dd  8285  ltsub1dd  8286  ltsub2dd  8287  leadd1dd  8288  leadd2dd  8289  lesub1dd  8290  lesub2dd  8291  recexre  8307  apreap  8316  ltmul1a  8320  reapmul1  8324  cru  8331  apreim  8332  mulge0  8348  leltap  8354  negap0d  8360  ltleap  8361  ltapd  8367  ap0gt0  8369  ap0gt0d  8370  subap0d  8373  mulcanapad  8391  mulcanap2ad  8392  eqnegad  8461  diveqap0d  8524  diveqap1d  8525  divap1d  8528  rec11apd  8538  div11apd  8558  div2subap  8563  recgt0  8572  prodgt0  8574  lemul1a  8580  lemulge12  8589  lt2msq1  8607  lediv12a  8616  recreclt  8622  nn1suc  8703  nnnlt1  8710  nn2ge  8717  nn1gt1  8718  nnrecl  8933  nn0nlt0  8961  elnn0z  9025  elz2  9080  nn0n0n1ge2b  9088  nnm1ge0  9095  nn0ge0div  9096  zextle  9100  suprzclex  9107  nn0ind-raph  9126  zindd  9127  uzneg  9300  eluzadd  9310  eluzsub  9311  uzm1  9312  uz3m2nn  9324  supminfex  9348  nn01to3  9365  ltrec1d  9459  lerec2d  9460  ledivdivd  9464  divge1  9465  ltmul1dd  9494  ltmul2dd  9495  ltdiv1dd  9496  lediv1dd  9497  ltdiv23d  9499  lediv23d  9500  nn0ledivnn  9509  addlelt  9510  xrlelttr  9544  xrltletr  9545  xaddass2  9608  xltadd1  9614  xlt2add  9618  ixxdisj  9641  icoshftf1o  9729  icodisj  9730  lincmb01cmp  9741  iccf1o  9742  uzsubsubfz  9782  fzdisj  9787  fzopth  9796  fznatpl1  9811  fzsuc2  9814  fzp1disj  9815  fzrev2i  9821  uzdisj  9828  fseq1p1m1  9829  fzm1  9835  fzneuz  9836  fzp1nel  9839  fzrevral  9840  fznn0sub2  9860  fz0fzdiffz0  9862  difelfzle  9866  difelfznle  9867  nn0disj  9870  fzonnsub  9901  fzodisj  9910  fzouzdisj  9912  eluzgtdifelfzo  9929  ubmelfzo  9932  fzonn0p1p1  9945  ubmelm1fzo  9958  fzostep1  9969  exfzdc  9972  subfzo0  9974  qtri3or  9975  exbtwnzlemex  9982  rebtwn2z  9987  qbtwnrelemcalc  9988  qbtwnre  9989  qavgle  9991  apbtwnz  10002  flid  10012  flqwordi  10016  flqmulnn0  10027  flhalf  10030  flltdivnn0lt  10032  fldiv4p1lem1div2  10033  intfracq  10048  flqdiv  10049  flqpmodeq  10055  modqmulnn  10070  mulqaddmodid  10092  modqmuladdim  10095  modqmuladdnn0  10096  m1modge3gt1  10099  q2submod  10113  modaddmodup  10115  modqsubdir  10121  modqeqmodmin  10122  modfzo0difsn  10123  uzennn  10164  uzsinds  10170  monoord2  10205  ser3mono  10206  iseqf1olemqcl  10214  iseqf1olemnab  10216  iseqf1olemab  10217  iseqf1olemqf1o  10221  iseqf1olemqk  10222  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1olemp  10230  ser3le  10246  exp3val  10250  expnegap0  10256  expgt1  10286  ltexp2a  10300  le2sq2  10323  nnlesq  10351  bernneq  10367  expnbnd  10370  expnlbnd  10371  expnlbnd2  10372  expeq0d  10375  sq11d  10412  expcand  10419  nn0opthd  10423  facdiv  10439  faclbnd6  10445  facubnd  10446  facavg  10447  bcval4  10453  bcp1nk  10463  bcval5  10464  bcpasc  10467  hashennnuni  10480  focdmex  10488  isfinite4im  10494  hashnncl  10497  hashunlem  10505  fiprsshashgt1  10518  hashfzp1  10525  zfz1isolemiso  10537  seq3coll  10540  seq3shft  10565  cjth  10573  cjdivap  10636  cjne0d  10674  cjap0d  10675  cvg1nlemcxze  10709  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniq  10722  resqrexlemover  10737  resqrexlemdecn  10739  resqrexlemlo  10740  resqrexlemcalc2  10742  resqrexlemcalc3  10743  resqrexlemnmsq  10744  resqrexlemnm  10745  resqrexlemcvg  10746  resqrexlemglsq  10749  resqrexlemga  10750  leabs  10801  absrele  10810  nn0abscl  10812  ltabs  10814  abslt  10815  absle  10816  abstri  10831  amgm2  10845  sqr11d  10900  abs00d  10913  maxabsle  10931  maxabslemlub  10934  maxleastlt  10942  maxltsup  10945  2zsupmax  10952  minmax  10956  xrmaxleim  10968  xrmaxiflemlub  10972  xrmaxiflemcom  10973  xrmaxiflemval  10974  xrmaxleastlt  10980  xrmaxltsup  10982  xrmaxaddlem  10984  xrmaxadd  10985  xrminmax  10989  xrmin1inf  10991  xrmin2inf  10992  xrmineqinf  10993  climi  11011  reccn2ap  11037  climge0  11049  climle  11058  climserle  11069  climrecvg1n  11072  fz1f1o  11099  summodclem3  11104  summodclem2a  11105  summodc  11107  fisumss  11116  fsum0diaglem  11164  mptfzshft  11166  fsumrev  11167  fisum0diag2  11171  fsumlessfi  11184  fsumle  11187  fsumlt  11188  isumsplit  11215  isumrpcl  11218  expcnvap0  11226  geosergap  11230  pwm1geoserap1  11232  absgtap  11234  geolim  11235  geolim2  11236  georeclim  11237  geoisumr  11242  geoisum1c  11244  cvgratnnlembern  11247  cvgratnnlemseq  11250  cvgratnnlemsumlt  11252  cvgratnnlemfm  11253  cvgratnnlemrate  11254  cvgratnn  11255  cvgratz  11256  mertenslemub  11258  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcllemp  11278  ege2le3  11291  eftlcvg  11307  eftlub  11310  efltim  11318  eflegeo  11322  tanaddap  11360  sinbnd  11373  cosbnd  11374  sin01bnd  11378  cos01bnd  11379  sin01gt0  11382  cos01gt0  11383  cos12dec  11388  eirraplem  11395  zdvdsdc  11426  dvdstr  11442  dvdsadd2b  11452  dvdslelemd  11453  divconjdvds  11459  alzdvds  11464  dvdsext  11465  fzm1ndvds  11466  fzo0dvdseq  11467  zeo3  11477  even2n  11483  mod2eq1n2dvds  11488  nn0ehalf  11512  nnehalf  11513  nno  11515  nn0oddm1d2  11518  divalglemnqt  11529  divalglemex  11531  divalglemeuneg  11532  divalg2  11535  divalgmod  11536  flodddiv4t2lthalf  11546  zsupcllemstep  11550  infssuzex  11554  dvdsbnd  11557  gcdsupex  11558  gcdsupcl  11559  gcddvds  11564  divgcdz  11572  divgcdnn  11575  gcd0id  11579  gcdneg  11582  gcd1  11587  dvdsgcdidd  11594  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmo  11606  bezoutlemsup  11609  dfgcd3  11610  bezout  11611  dfgcd2  11614  mulgcd  11616  sqgcd  11629  dvdssqlem  11630  bezoutr1  11633  lcmval  11656  lcmcllem  11660  dvdslcm  11662  lcmgcdlem  11670  lcmdvds  11672  lcmgcdeq  11676  ncoprmgcdne1b  11682  mulgcddvds  11687  rpmulgcd2  11688  qredeu  11690  rpdvds  11692  prmind2  11713  nprm  11716  dvdsnprmd  11718  divgcdodd  11733  isprm6  11737  prmexpb  11741  pw2dvds  11755  pw2dvdseulemle  11756  oddpwdclemdc  11762  sqne2sq  11766  znege1  11767  sqrt2irraplemnn  11768  divnumden  11785  divdenle  11786  qden1elz  11794  nn0sqrtelqelz  11795  hashdvds  11808  crth  11811  phimullem  11812  hashgcdlem  11814  oddennn  11816  ennnfonelemk  11824  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ennnfonelemex  11838  ennnfonelemhom  11839  ennnfonelemrnh  11840  ennnfonelemen  11845  ennnfonelemim  11848  ctinfomlemom  11851  ctiunctlemf  11862  ntridm  12206  ntrtop  12208  ntrcls0  12211  ntr0  12214  isopn3i  12215  neiss2  12222  opnneiss  12238  topssnei  12242  cnpf2  12287  icnpimaex  12291  lmcvg  12297  iscnp4  12298  cncnp  12310  cnptopresti  12318  lmfss  12324  lmtopcnp  12330  hmeores  12395  bldisj  12481  xblss2ps  12484  xblss2  12485  blhalf  12488  blssps  12507  blss  12508  ssblex  12511  blpnfctr  12519  xmetresbl  12520  mopni2  12563  bdxmet  12581  bdbl  12583  xmetxpbl  12588  metcnpi  12595  metcnpi2  12596  tgioo  12626  rescncf  12648  mulcncflem  12670  cnopnap  12674  dedekindeulemuub  12675  dedekindeulemloc  12677  dedekindeulemlu  12679  dedekindeu  12681  dedekindicclemuub  12684  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicclemicc  12690  dedekindicc  12691  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthdec  12702  limcimolemlt  12713  cnplimcim  12716  cnplimclemr  12718  limccnpcntop  12724  limccnp2cntop  12726  limccoap  12727  dvfgg  12737  dvidlemap  12740  dvaddxxbr  12745  dvmulxxbr  12746  dvaddxx  12747  dvmulxx  12748  dviaddf  12749  dvimulf  12750  dvcoapbr  12751  dvcjbr  12752  dvcj  12753  dvrecap  12757  dvmptclx  12760  dveflem  12766  sin0pilem1  12773  pilem3  12775  cosq14gt0  12824  coseq0negpitopi  12828  pwf1oexmid  13090  subctctexmid  13092  nnsf  13095  peano4nninf  13096  nninfalllemn  13098  nninfsellemeq  13106  cvgcmp2nlemabs  13123  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130  supfz  13133  inffz  13134
  Copyright terms: Public domain W3C validator