ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbid GIF 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 (𝜑𝜓)
mpbid.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbid (𝜑𝜒)

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2 (𝜑𝜓)
2 mpbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 143 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
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  921  mpbi2and  927  bilukdc  1374  equs5or  1802  eqtrd  2172  eleqtrd  2218  neeqtrd  2336  3netr3d  2340  rexlimd2  2547  ceqsalt  2712  vtoclgft  2736  vtoclegft  2758  elrab3t  2839  eueq2dc  2857  sbceq1dd  2915  csbiedf  3040  sseqtrd  3135  3sstr3d  3141  ifbothdadc  3503  snssd  3665  dfnfc2  3754  breqdi  3944  breqtrd  3954  3brtr3d  3959  csbexga  4056  reuhypd  4392  reg2exmidlema  4449  elirr  4456  en2lp  4469  onsucuni2  4479  finds  4514  iota4  5106  iota4an  5107  funimaexglem  5206  fneu  5227  fco2  5289  fssres2  5300  fresin  5301  feu  5305  f1orescnv  5383  resdif  5389  funcocnv2  5392  f1oprg  5411  fvelrnb  5469  fimacnv  5549  f1oresrab  5585  fsn2  5594  xpsng  5595  fnressn  5606  fsnunf  5620  foeqcnvco  5691  isores1  5715  isoini2  5720  riota5f  5754  riotass2  5756  riotass  5757  ovmpodxf  5896  elopabi  6093  cnvf1o  6122  smores3  6190  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  rdgon  6283  frecabcl  6296  frecsuclem  6303  nnsucsssuc  6388  nnsucuniel  6391  erref  6449  iserd  6455  swoer  6457  swoord1  6458  swoord2  6459  erth  6473  erthi  6475  eroveu  6520  pmresg  6570  mapsn  6584  fndmeng  6704  xpen  6739  phplem4  6749  phplem4on  6761  fidifsnen  6764  dif1en  6773  dif1enen  6774  fisbth  6777  diffisn  6787  ac6sfi  6792  fimax2gtri  6795  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  fiintim  6817  fidcenumlemrks  6841  elfi2  6860  elfir  6861  fiuni  6866  fifo  6868  eqsupti  6883  supisoti  6897  ordiso2  6920  casef  6973  difinfsnlem  6984  ctmlemr  6993  ctssdccl  6996  enumct  7000  enomnilem  7010  exmidomni  7014  fodjum  7018  fodjuomnilemres  7020  mkvprop  7032  acfun  7068  ccfunen  7084  cc2lem  7086  dfplpq2  7174  ltanqi  7222  ltmnqi  7223  ltaddnq  7227  subhalfnqq  7234  ltbtwnnqq  7235  archnqq  7237  prarloclemarch2  7239  enq0sym  7252  enq0ref  7253  enq0tr  7254  nqnq0pi  7258  nnnq0lem1  7266  distrnq0  7279  prarloclemlt  7313  prarloclemn  7319  prarloclemcalc  7322  genplt2i  7330  addnqprllem  7347  addnqprulem  7348  addlocprlemgt  7354  appdivnq  7383  prmuloc2  7387  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemru  7432  prplnqu  7440  cauappcvgprlemopl  7466  cauappcvgprlemlol  7467  cauappcvgprlemladdfu  7474  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  archrecnq  7483  archrecpr  7484  caucvgprlemk  7485  caucvgprlemnbj  7487  caucvgprlemm  7488  caucvgprlemopl  7489  caucvgprlemlol  7490  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  caucvgprlem1  7499  caucvgprprlemk  7503  caucvgprprlemnkeqj  7510  caucvgprprlemnbj  7513  caucvgprprlemml  7514  caucvgprprlemmu  7515  caucvgprprlemopl  7517  caucvgprprlemlol  7518  caucvgprprlemopu  7519  caucvgprprlemexbt  7526  caucvgprprlemexb  7527  caucvgprprlem1  7529  caucvgprprlem2  7530  suplocexprlemru  7539  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  suplocexprlemlub  7544  prsrlem1  7562  addgt0sr  7595  srpospr  7603  prsrriota  7608  caucvgsrlemgt1  7615  caucvgsrlemoffgt1  7619  caucvgsr  7622  mappsrprg  7624  suplocsrlemb  7626  suplocsrlempr  7627  suplocsrlem  7628  recriota  7710  axsuploc  7849  lelttr  7864  ltletr  7865  ltnsymd  7894  lensymd  7896  cnegexlem3  7951  cnegex2  7953  addcanad  7960  addcan2ad  7961  negcon1ad  8080  negne0d  8083  negrebd  8084  subeq0d  8093  subne0ad  8096  neg11d  8097  subcand  8126  subcan2d  8127  ltadd2  8193  ltadd2dd  8196  add20  8248  ltnegcon1d  8299  ltnegcon2d  8300  lenegcon1d  8301  lenegcon2d  8302  subled  8322  lesubd  8323  ltsub23d  8324  ltsub13d  8325  ltadd1dd  8330  ltsub1dd  8331  ltsub2dd  8332  leadd1dd  8333  leadd2dd  8334  lesub1dd  8335  lesub2dd  8336  recexre  8352  apreap  8361  ltmul1a  8365  reapmul1  8369  cru  8376  apreim  8377  mulge0  8393  leltap  8399  negap0d  8405  ltleap  8406  ltapd  8412  ap0gt0  8414  ap0gt0d  8415  subap0d  8418  mulcanapad  8436  mulcanap2ad  8437  eqnegad  8506  diveqap0d  8569  diveqap1d  8570  divap1d  8573  rec11apd  8583  div11apd  8603  div2subap  8608  recgt0  8620  prodgt0  8622  lemul1a  8628  lemulge12  8637  lt2msq1  8655  lediv12a  8664  recreclt  8670  nn1suc  8751  nnnlt1  8758  nn2ge  8765  nn1gt1  8766  nnrecl  8987  nn0nlt0  9015  elnn0z  9079  elz2  9134  nn0n0n1ge2b  9142  nnm1ge0  9149  nn0ge0div  9150  zextle  9154  suprzclex  9161  nn0ind-raph  9180  zindd  9181  uzneg  9356  eluzadd  9366  eluzsub  9367  uzm1  9368  uz3m2nn  9380  supminfex  9404  nn01to3  9421  ltrec1d  9516  lerec2d  9517  ledivdivd  9521  divge1  9522  ltmul1dd  9551  ltmul2dd  9552  ltdiv1dd  9553  lediv1dd  9554  ltdiv23d  9556  lediv23d  9557  nn0ledivnn  9566  addlelt  9567  xrlelttr  9601  xrltletr  9602  xaddass2  9665  xltadd1  9671  xlt2add  9675  ixxdisj  9698  icoshftf1o  9786  icodisj  9787  lincmb01cmp  9798  iccf1o  9799  uzsubsubfz  9839  fzdisj  9844  fzopth  9853  fznatpl1  9868  fzsuc2  9871  fzp1disj  9872  fzrev2i  9878  uzdisj  9885  fseq1p1m1  9886  fzm1  9892  fzneuz  9893  fzp1nel  9896  fzrevral  9897  fznn0sub2  9917  fz0fzdiffz0  9919  difelfzle  9923  difelfznle  9924  nn0disj  9927  fzonnsub  9958  fzodisj  9967  fzouzdisj  9969  eluzgtdifelfzo  9986  ubmelfzo  9989  fzonn0p1p1  10002  ubmelm1fzo  10015  fzostep1  10026  exfzdc  10029  subfzo0  10031  qtri3or  10032  exbtwnzlemex  10039  rebtwn2z  10044  qbtwnrelemcalc  10045  qbtwnre  10046  qavgle  10048  apbtwnz  10059  flid  10069  flqwordi  10073  flqmulnn0  10084  flhalf  10087  flltdivnn0lt  10089  fldiv4p1lem1div2  10090  intfracq  10105  flqdiv  10106  flqpmodeq  10112  modqmulnn  10127  mulqaddmodid  10149  modqmuladdim  10152  modqmuladdnn0  10153  m1modge3gt1  10156  q2submod  10170  modaddmodup  10172  modqsubdir  10178  modqeqmodmin  10179  modfzo0difsn  10180  uzennn  10221  uzsinds  10227  monoord2  10262  ser3mono  10263  iseqf1olemqcl  10271  iseqf1olemnab  10273  iseqf1olemab  10274  iseqf1olemqf1o  10278  iseqf1olemqk  10279  seq3f1olemqsumkj  10283  seq3f1olemqsumk  10284  seq3f1olemqsum  10285  seq3f1olemp  10287  ser3le  10303  exp3val  10307  expnegap0  10313  expgt1  10343  ltexp2a  10357  le2sq2  10380  nnlesq  10408  bernneq  10424  expnbnd  10427  expnlbnd  10428  expnlbnd2  10429  expeq0d  10432  sq11d  10469  expcand  10476  nn0opthd  10480  facdiv  10496  faclbnd6  10502  facubnd  10503  facavg  10504  bcval4  10510  bcp1nk  10520  bcval5  10521  bcpasc  10524  hashennnuni  10537  focdmex  10545  isfinite4im  10551  hashnncl  10554  hashunlem  10562  fiprsshashgt1  10575  hashfzp1  10582  zfz1isolemiso  10594  seq3coll  10597  seq3shft  10622  cjth  10630  cjdivap  10693  cjne0d  10731  cjap0d  10732  cvg1nlemcxze  10766  cvg1nlemcau  10768  cvg1nlemres  10769  recvguniq  10779  resqrexlemover  10794  resqrexlemdecn  10796  resqrexlemlo  10797  resqrexlemcalc2  10799  resqrexlemcalc3  10800  resqrexlemnmsq  10801  resqrexlemnm  10802  resqrexlemcvg  10803  resqrexlemglsq  10806  resqrexlemga  10807  leabs  10858  absrele  10867  nn0abscl  10869  ltabs  10871  abslt  10872  absle  10873  abstri  10888  amgm2  10902  sqr11d  10957  abs00d  10970  maxabsle  10988  maxabslemlub  10991  maxleastlt  10999  maxltsup  11002  2zsupmax  11009  minmax  11013  xrmaxleim  11025  xrmaxiflemlub  11029  xrmaxiflemcom  11030  xrmaxiflemval  11031  xrmaxleastlt  11037  xrmaxltsup  11039  xrmaxaddlem  11041  xrmaxadd  11042  xrminmax  11046  xrmin1inf  11048  xrmin2inf  11049  xrmineqinf  11050  climi  11068  reccn2ap  11094  climge0  11106  climle  11115  climserle  11126  climrecvg1n  11129  fz1f1o  11156  summodclem3  11161  summodclem2a  11162  summodc  11164  fisumss  11173  fsum0diaglem  11221  mptfzshft  11223  fsumrev  11224  fisum0diag2  11228  fsumlessfi  11241  fsumle  11244  fsumlt  11245  isumsplit  11272  isumrpcl  11275  expcnvap0  11283  geosergap  11287  pwm1geoserap1  11289  absgtap  11291  geolim  11292  geolim2  11293  georeclim  11294  geoisumr  11299  geoisum1c  11301  cvgratnnlembern  11304  cvgratnnlemseq  11307  cvgratnnlemsumlt  11309  cvgratnnlemfm  11310  cvgratnnlemrate  11311  cvgratnn  11312  cvgratz  11313  mertenslemub  11315  mertenslemi1  11316  mertenslem2  11317  mertensabs  11318  prodmodclem2a  11357  prodmodc  11359  efcllemp  11376  ege2le3  11389  eftlcvg  11405  eftlub  11408  efltim  11416  eflegeo  11419  tanaddap  11457  sinbnd  11470  cosbnd  11471  sin01bnd  11475  cos01bnd  11476  sin01gt0  11479  cos01gt0  11480  cos12dec  11485  eirraplem  11494  zdvdsdc  11525  dvdstr  11541  dvdsadd2b  11551  dvdslelemd  11552  divconjdvds  11558  alzdvds  11563  dvdsext  11564  fzm1ndvds  11565  fzo0dvdseq  11566  zeo3  11576  even2n  11582  mod2eq1n2dvds  11587  nn0ehalf  11611  nnehalf  11612  nno  11614  nn0oddm1d2  11617  divalglemnqt  11628  divalglemex  11630  divalglemeuneg  11631  divalg2  11634  divalgmod  11635  flodddiv4t2lthalf  11645  zsupcllemstep  11649  infssuzex  11653  dvdsbnd  11656  gcdsupex  11657  gcdsupcl  11658  gcddvds  11663  divgcdz  11671  divgcdnn  11674  gcd0id  11678  gcdneg  11681  gcd1  11686  dvdsgcdidd  11693  bezoutlemnewy  11695  bezoutlemstep  11696  bezoutlemmo  11705  bezoutlemsup  11708  dfgcd3  11709  bezout  11710  dfgcd2  11713  mulgcd  11715  sqgcd  11728  dvdssqlem  11729  bezoutr1  11732  lcmval  11755  lcmcllem  11759  dvdslcm  11761  lcmgcdlem  11769  lcmdvds  11771  lcmgcdeq  11775  ncoprmgcdne1b  11781  mulgcddvds  11786  rpmulgcd2  11787  qredeu  11789  rpdvds  11791  prmind2  11812  nprm  11815  dvdsnprmd  11817  divgcdodd  11832  isprm6  11836  prmexpb  11840  pw2dvds  11855  pw2dvdseulemle  11856  oddpwdclemdc  11862  sqne2sq  11866  znege1  11867  sqrt2irraplemnn  11868  divnumden  11885  divdenle  11886  qden1elz  11894  nn0sqrtelqelz  11895  hashdvds  11908  crth  11911  phimullem  11912  hashgcdlem  11914  oddennn  11916  ennnfonelemk  11924  ennnfonelemkh  11936  ennnfonelemhf1o  11937  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemrnh  11940  ennnfonelemen  11945  ennnfonelemim  11948  ctinfomlemom  11951  ctiunctlemf  11962  ntridm  12309  ntrtop  12311  ntrcls0  12314  ntr0  12317  isopn3i  12318  neiss2  12325  opnneiss  12341  topssnei  12345  cnpf2  12390  icnpimaex  12394  lmcvg  12400  iscnp4  12401  cncnp  12413  cnptopresti  12421  lmfss  12427  lmtopcnp  12433  hmeores  12498  bldisj  12584  xblss2ps  12587  xblss2  12588  blhalf  12591  blssps  12610  blss  12611  ssblex  12614  blpnfctr  12622  xmetresbl  12623  mopni2  12666  bdxmet  12684  bdbl  12686  xmetxpbl  12691  metcnpi  12698  metcnpi2  12699  tgioo  12729  rescncf  12751  mulcncflem  12773  cnopnap  12777  dedekindeulemuub  12778  dedekindeulemloc  12780  dedekindeulemlu  12782  dedekindeu  12784  dedekindicclemuub  12787  dedekindicclemloc  12789  dedekindicclemlu  12791  dedekindicclemicc  12793  dedekindicc  12794  ivthinclemlopn  12797  ivthinclemuopn  12799  ivthdec  12805  limcimolemlt  12816  cnplimcim  12819  cnplimclemr  12821  limccnpcntop  12827  limccnp2cntop  12829  limccoap  12830  dvfgg  12840  dvidlemap  12843  dvaddxxbr  12848  dvmulxxbr  12849  dvaddxx  12850  dvmulxx  12851  dviaddf  12852  dvimulf  12853  dvcoapbr  12854  dvcjbr  12855  dvcj  12856  dvrecap  12860  dvmptclx  12863  dveflem  12870  reeff1oleme  12876  eflt  12879  sin0pilem1  12884  pilem3  12886  cosq14gt0  12935  coseq0negpitopi  12939  tangtx  12941  coskpi  12951  cosordlem  12952  cosq34lt1  12953  relogef  12965  rplogcl  12977  logge0  12978  logdivlti  12979  pwf1oexmid  13253  subctctexmid  13255  pw1nct  13257  nnsf  13260  peano4nninf  13261  nninfalllemn  13263  nninfsellemeq  13271  cvgcmp2nlemabs  13288  trilpolemisumle  13292  trilpolemeq1  13294  trilpolemlt1  13295  trirec0  13298  apdifflemf  13300  apdifflemr  13301  apdiff  13302  supfz  13303  inffz  13304
  Copyright terms: Public domain W3C validator