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  904  mpbi2and  910  bilukdc  1357  equs5or  1784  eqtrd  2148  eleqtrd  2194  neeqtrd  2311  3netr3d  2315  rexlimd2  2522  ceqsalt  2684  vtoclgft  2708  vtoclegft  2730  elrab3t  2810  eueq2dc  2828  sbceq1dd  2886  csbiedf  3008  sseqtrd  3103  3sstr3d  3109  ifbothdadc  3471  snssd  3633  dfnfc2  3722  breqdi  3912  breqtrd  3922  3brtr3d  3927  csbexga  4024  reuhypd  4360  reg2exmidlema  4417  elirr  4424  en2lp  4437  onsucuni2  4447  finds  4482  iota4  5074  iota4an  5075  funimaexglem  5174  fneu  5195  fco2  5257  fssres2  5268  fresin  5269  feu  5273  f1orescnv  5349  resdif  5355  funcocnv2  5358  f1oprg  5377  fvelrnb  5435  fimacnv  5515  f1oresrab  5551  fsn2  5560  xpsng  5561  fnressn  5572  fsnunf  5586  foeqcnvco  5657  isores1  5681  isoini2  5686  riota5f  5720  riotass2  5722  riotass  5723  ovmpodxf  5862  elopabi  6059  cnvf1o  6088  smores3  6156  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  rdgon  6249  frecabcl  6262  frecsuclem  6269  nnsucsssuc  6354  nnsucuniel  6357  erref  6415  iserd  6421  swoer  6423  swoord1  6424  swoord2  6425  erth  6439  erthi  6441  eroveu  6486  pmresg  6536  mapsn  6550  fndmeng  6670  xpen  6705  phplem4  6715  phplem4on  6727  fidifsnen  6730  dif1en  6739  dif1enen  6740  fisbth  6743  diffisn  6753  ac6sfi  6758  fimax2gtri  6761  en2eqpr  6767  unsnfidcex  6774  unsnfidcel  6775  fiintim  6783  fidcenumlemrks  6807  elfi2  6826  elfir  6827  fiuni  6832  fifo  6834  eqsupti  6849  supisoti  6863  ordiso2  6886  casef  6939  difinfsnlem  6950  ctmlemr  6959  ctssdccl  6962  enumct  6966  enomnilem  6976  exmidomni  6980  fodjum  6984  fodjuomnilemres  6986  mkvprop  6998  acfun  7027  ccfunen  7043  dfplpq2  7126  ltanqi  7174  ltmnqi  7175  ltaddnq  7179  subhalfnqq  7186  ltbtwnnqq  7187  archnqq  7189  prarloclemarch2  7191  enq0sym  7204  enq0ref  7205  enq0tr  7206  nqnq0pi  7210  nnnq0lem1  7218  distrnq0  7231  prarloclemlt  7265  prarloclemn  7271  prarloclemcalc  7274  genplt2i  7282  addnqprllem  7299  addnqprulem  7300  addlocprlemgt  7306  appdivnq  7335  prmuloc2  7339  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemru  7384  prplnqu  7392  cauappcvgprlemopl  7418  cauappcvgprlemlol  7419  cauappcvgprlemladdfu  7426  cauappcvgprlemladdrl  7429  cauappcvgprlem1  7431  archrecnq  7435  archrecpr  7436  caucvgprlemk  7437  caucvgprlemnbj  7439  caucvgprlemm  7440  caucvgprlemopl  7441  caucvgprlemlol  7442  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlem1  7451  caucvgprprlemk  7455  caucvgprprlemnkeqj  7462  caucvgprprlemnbj  7465  caucvgprprlemml  7466  caucvgprprlemmu  7467  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemopu  7471  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgprprlem1  7481  caucvgprprlem2  7482  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  suplocexprlemlub  7496  prsrlem1  7514  addgt0sr  7547  srpospr  7555  prsrriota  7560  caucvgsrlemgt1  7567  caucvgsrlemoffgt1  7571  caucvgsr  7574  mappsrprg  7576  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  recriota  7662  axsuploc  7801  lelttr  7816  ltletr  7817  ltnsymd  7846  lensymd  7848  cnegexlem3  7903  cnegex2  7905  addcanad  7912  addcan2ad  7913  negcon1ad  8032  negne0d  8035  negrebd  8036  subeq0d  8045  subne0ad  8048  neg11d  8049  subcand  8078  subcan2d  8079  ltadd2  8145  ltadd2dd  8148  add20  8200  ltnegcon1d  8250  ltnegcon2d  8251  lenegcon1d  8252  lenegcon2d  8253  subled  8273  lesubd  8274  ltsub23d  8275  ltsub13d  8276  ltadd1dd  8281  ltsub1dd  8282  ltsub2dd  8283  leadd1dd  8284  leadd2dd  8285  lesub1dd  8286  lesub2dd  8287  recexre  8303  apreap  8312  ltmul1a  8316  reapmul1  8320  cru  8327  apreim  8328  mulge0  8344  leltap  8350  ltleap  8356  ltapd  8362  ap0gt0  8364  ap0gt0d  8365  subap0d  8368  mulcanapad  8384  mulcanap2ad  8385  eqnegad  8454  diveqap0d  8517  diveqap1d  8518  divap1d  8521  rec11apd  8531  div11apd  8551  div2subap  8556  recgt0  8565  prodgt0  8567  lemul1a  8573  lemulge12  8582  lt2msq1  8600  lediv12a  8609  recreclt  8615  nn1suc  8696  nnnlt1  8703  nn2ge  8710  nn1gt1  8711  nnrecl  8926  nn0nlt0  8954  elnn0z  9018  elz2  9073  nn0n0n1ge2b  9081  nnm1ge0  9088  nn0ge0div  9089  zextle  9093  suprzclex  9100  nn0ind-raph  9119  zindd  9120  uzneg  9293  eluzadd  9303  eluzsub  9304  uzm1  9305  uz3m2nn  9317  supminfex  9341  nn01to3  9358  ltrec1d  9450  lerec2d  9451  ledivdivd  9455  divge1  9456  ltmul1dd  9485  ltmul2dd  9486  ltdiv1dd  9487  lediv1dd  9488  ltdiv23d  9490  lediv23d  9491  nn0ledivnn  9494  addlelt  9495  xrlelttr  9529  xrltletr  9530  xaddass2  9593  xltadd1  9599  xlt2add  9603  ixxdisj  9626  icoshftf1o  9714  icodisj  9715  lincmb01cmp  9726  iccf1o  9727  uzsubsubfz  9767  fzdisj  9772  fzopth  9781  fznatpl1  9796  fzsuc2  9799  fzp1disj  9800  fzrev2i  9806  uzdisj  9813  fseq1p1m1  9814  fzm1  9820  fzneuz  9821  fzp1nel  9824  fzrevral  9825  fznn0sub2  9845  fz0fzdiffz0  9847  difelfzle  9851  difelfznle  9852  nn0disj  9855  fzonnsub  9886  fzodisj  9895  fzouzdisj  9897  eluzgtdifelfzo  9914  ubmelfzo  9917  fzonn0p1p1  9930  ubmelm1fzo  9943  fzostep1  9954  exfzdc  9957  subfzo0  9959  qtri3or  9960  exbtwnzlemex  9967  rebtwn2z  9972  qbtwnrelemcalc  9973  qbtwnre  9974  qavgle  9976  apbtwnz  9987  flid  9997  flqwordi  10001  flqmulnn0  10012  flhalf  10015  flltdivnn0lt  10017  fldiv4p1lem1div2  10018  intfracq  10033  flqdiv  10034  flqpmodeq  10040  modqmulnn  10055  mulqaddmodid  10077  modqmuladdim  10080  modqmuladdnn0  10081  m1modge3gt1  10084  q2submod  10098  modaddmodup  10100  modqsubdir  10106  modqeqmodmin  10107  modfzo0difsn  10108  uzennn  10149  uzsinds  10155  monoord2  10190  ser3mono  10191  iseqf1olemqcl  10199  iseqf1olemnab  10201  iseqf1olemab  10202  iseqf1olemqf1o  10206  iseqf1olemqk  10207  seq3f1olemqsumkj  10211  seq3f1olemqsumk  10212  seq3f1olemqsum  10213  seq3f1olemp  10215  ser3le  10231  exp3val  10235  expnegap0  10241  expgt1  10271  ltexp2a  10285  le2sq2  10308  nnlesq  10336  bernneq  10352  expnbnd  10355  expnlbnd  10356  expnlbnd2  10357  expeq0d  10360  sq11d  10397  expcand  10404  nn0opthd  10408  facdiv  10424  faclbnd6  10430  facubnd  10431  facavg  10432  bcval4  10438  bcp1nk  10448  bcval5  10449  bcpasc  10452  hashennnuni  10465  focdmex  10473  isfinite4im  10479  hashnncl  10482  hashunlem  10490  fiprsshashgt1  10503  hashfzp1  10510  zfz1isolemiso  10522  seq3coll  10525  seq3shft  10550  cjth  10558  cjdivap  10621  cjne0d  10659  cjap0d  10660  cvg1nlemcxze  10694  cvg1nlemcau  10696  cvg1nlemres  10697  recvguniq  10707  resqrexlemover  10722  resqrexlemdecn  10724  resqrexlemlo  10725  resqrexlemcalc2  10727  resqrexlemcalc3  10728  resqrexlemnmsq  10729  resqrexlemnm  10730  resqrexlemcvg  10731  resqrexlemglsq  10734  resqrexlemga  10735  leabs  10786  absrele  10795  nn0abscl  10797  ltabs  10799  abslt  10800  absle  10801  abstri  10816  amgm2  10830  sqr11d  10885  abs00d  10898  maxabsle  10916  maxabslemlub  10919  maxleastlt  10927  maxltsup  10930  2zsupmax  10937  minmax  10941  xrmaxleim  10953  xrmaxiflemlub  10957  xrmaxiflemcom  10958  xrmaxiflemval  10959  xrmaxleastlt  10965  xrmaxltsup  10967  xrmaxaddlem  10969  xrmaxadd  10970  xrminmax  10974  xrmin1inf  10976  xrmin2inf  10977  xrmineqinf  10978  climi  10996  reccn2ap  11022  climge0  11034  climle  11043  climserle  11054  climrecvg1n  11057  fz1f1o  11084  summodclem3  11089  summodclem2a  11090  summodc  11092  fisumss  11101  fsum0diaglem  11149  mptfzshft  11151  fsumrev  11152  fisum0diag2  11156  fsumlessfi  11169  fsumle  11172  fsumlt  11173  isumsplit  11200  isumrpcl  11203  expcnvap0  11211  geosergap  11215  pwm1geoserap1  11217  absgtap  11219  geolim  11220  geolim2  11221  georeclim  11222  geoisumr  11227  geoisum1c  11229  cvgratnnlembern  11232  cvgratnnlemseq  11235  cvgratnnlemsumlt  11237  cvgratnnlemfm  11238  cvgratnnlemrate  11239  cvgratnn  11240  cvgratz  11241  mertenslemub  11243  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  efcllemp  11263  ege2le3  11276  eftlcvg  11292  eftlub  11295  efltim  11303  eflegeo  11307  tanaddap  11345  sinbnd  11358  cosbnd  11359  sin01bnd  11363  cos01bnd  11364  sin01gt0  11367  cos01gt0  11368  eirraplem  11379  zdvdsdc  11410  dvdstr  11426  dvdsadd2b  11436  dvdslelemd  11437  divconjdvds  11443  alzdvds  11448  dvdsext  11449  fzm1ndvds  11450  fzo0dvdseq  11451  zeo3  11461  even2n  11467  mod2eq1n2dvds  11472  nn0ehalf  11496  nnehalf  11497  nno  11499  nn0oddm1d2  11502  divalglemnqt  11513  divalglemex  11515  divalglemeuneg  11516  divalg2  11519  divalgmod  11520  flodddiv4t2lthalf  11530  zsupcllemstep  11534  infssuzex  11538  dvdsbnd  11541  gcdsupex  11542  gcdsupcl  11543  gcddvds  11548  divgcdz  11556  divgcdnn  11559  gcd0id  11563  gcdneg  11566  gcd1  11571  dvdsgcdidd  11578  bezoutlemnewy  11580  bezoutlemstep  11581  bezoutlemmo  11590  bezoutlemsup  11593  dfgcd3  11594  bezout  11595  dfgcd2  11598  mulgcd  11600  sqgcd  11613  dvdssqlem  11614  bezoutr1  11617  lcmval  11640  lcmcllem  11644  dvdslcm  11646  lcmgcdlem  11654  lcmdvds  11656  lcmgcdeq  11660  ncoprmgcdne1b  11666  mulgcddvds  11671  rpmulgcd2  11672  qredeu  11674  rpdvds  11676  prmind2  11697  nprm  11700  dvdsnprmd  11702  divgcdodd  11717  isprm6  11721  prmexpb  11725  pw2dvds  11739  pw2dvdseulemle  11740  oddpwdclemdc  11746  sqne2sq  11750  znege1  11751  sqrt2irraplemnn  11752  divnumden  11769  divdenle  11770  qden1elz  11778  nn0sqrtelqelz  11779  hashdvds  11792  crth  11795  phimullem  11796  hashgcdlem  11798  oddennn  11800  ennnfonelemk  11808  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ennnfonelemex  11822  ennnfonelemhom  11823  ennnfonelemrnh  11824  ennnfonelemen  11829  ennnfonelemim  11832  ctinfomlemom  11835  ctiunctlemf  11846  ntridm  12190  ntrtop  12192  ntrcls0  12195  ntr0  12198  isopn3i  12199  neiss2  12206  opnneiss  12222  topssnei  12226  cnpf2  12271  icnpimaex  12275  lmcvg  12281  iscnp4  12282  cncnp  12294  cnptopresti  12302  lmfss  12308  lmtopcnp  12314  hmeores  12379  bldisj  12465  xblss2ps  12468  xblss2  12469  blhalf  12472  blssps  12491  blss  12492  ssblex  12495  blpnfctr  12503  xmetresbl  12504  mopni2  12547  bdxmet  12565  bdbl  12567  xmetxpbl  12572  metcnpi  12579  metcnpi2  12580  tgioo  12610  rescncf  12632  mulcncflem  12654  cnopnap  12658  dedekindeulemuub  12659  dedekindeulemloc  12661  dedekindeulemlu  12663  dedekindeu  12665  dedekindicclemuub  12668  dedekindicclemloc  12670  dedekindicclemlu  12672  dedekindicc  12674  limcimolemlt  12685  cnplimcim  12688  cnplimclemr  12690  limccnpcntop  12696  limccnp2cntop  12698  limccoap  12699  dvfgg  12709  dvidlemap  12712  dvaddxxbr  12717  dvmulxxbr  12718  dvaddxx  12719  dvmulxx  12720  dviaddf  12721  dvimulf  12722  dvcoapbr  12723  dvcjbr  12724  dvcj  12725  dvrecap  12729  dvmptclx  12732  dveflem  12738  pwf1oexmid  13005  subctctexmid  13007  nnsf  13010  peano4nninf  13011  nninfalllemn  13013  nninfsellemeq  13021  cvgcmp2nlemabs  13038  trilpolemisumle  13042  trilpolemeq1  13044  trilpolemlt1  13045  supfz  13048  inffz  13049
  Copyright terms: Public domain W3C validator