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

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2 (𝜑𝜓)
2 mpbid.maj . . 3 (𝜑 → (𝜓𝜒))
32biimpd 142 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
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  3941  reuhypd  4266  reg2exmidlema  4322  elirr  4329  en2lp  4342  onsucuni2  4352  finds  4387  iota4  4961  iota4an  4962  funimaexglem  5059  fneu  5080  fco2  5135  fssres2  5145  fresin  5146  feu  5150  f1orescnv  5226  resdif  5232  funcocnv2  5235  f1oprg  5252  fvelrnb  5309  fimacnv  5385  f1oresrab  5420  fsn2  5428  xpsng  5429  fnressn  5440  fsnunf  5453  foeqcnvco  5524  isores1  5548  isoini2  5553  riota5f  5587  riotass2  5589  riotass  5590  ovmpt2dxf  5721  elopabi  5916  cnvf1o  5941  smores3  6006  tfrlemisucaccv  6038  tfr1onlemsucaccv  6054  tfrcllemsucaccv  6067  rdgon  6099  frecabcl  6112  frecsuclem  6119  nnsucsssuc  6201  nnsucuniel  6204  erref  6258  iserd  6264  swoer  6266  swoord1  6267  swoord2  6268  erth  6282  erthi  6284  eroveu  6329  pmresg  6379  mapsn  6393  fndmeng  6473  xpen  6507  phplem4  6517  phplem4on  6529  fidifsnen  6532  dif1en  6541  dif1enen  6542  fisbth  6545  diffisn  6555  ac6sfi  6560  fimax2gtri  6563  en2eqpr  6569  unsnfidcex  6576  unsnfidcel  6577  eqsupti  6628  supisoti  6642  ordiso2  6665  djur  6694  casef  6716  enomnilem  6731  exmidomni  6735  fodjuomnilemm  6738  fodjuomnilemres  6740  dfplpq2  6850  ltanqi  6898  ltmnqi  6899  ltaddnq  6903  subhalfnqq  6910  ltbtwnnqq  6911  archnqq  6913  prarloclemarch2  6915  enq0sym  6928  enq0ref  6929  enq0tr  6930  nqnq0pi  6934  nnnq0lem1  6942  distrnq0  6955  prarloclemlt  6989  prarloclemn  6995  prarloclemcalc  6998  genplt2i  7006  addnqprllem  7023  addnqprulem  7024  addlocprlemgt  7030  appdivnq  7059  prmuloc2  7063  ltexprlemopl  7097  ltexprlemopu  7099  ltexprlemru  7108  prplnqu  7116  cauappcvgprlemopl  7142  cauappcvgprlemlol  7143  cauappcvgprlemladdfu  7150  cauappcvgprlemladdrl  7153  cauappcvgprlem1  7155  archrecnq  7159  archrecpr  7160  caucvgprlemk  7161  caucvgprlemnbj  7163  caucvgprlemm  7164  caucvgprlemopl  7165  caucvgprlemlol  7166  caucvgprlemladdfu  7173  caucvgprlemladdrl  7174  caucvgprlem1  7175  caucvgprprlemk  7179  caucvgprprlemnkeqj  7186  caucvgprprlemnbj  7189  caucvgprprlemml  7190  caucvgprprlemmu  7191  caucvgprprlemopl  7193  caucvgprprlemlol  7194  caucvgprprlemopu  7195  caucvgprprlemexbt  7202  caucvgprprlemexb  7203  caucvgprprlem1  7205  caucvgprprlem2  7206  prsrlem1  7225  addgt0sr  7258  srpospr  7265  prsrriota  7270  caucvgsrlemgt1  7277  caucvgsrlemoffgt1  7281  caucvgsr  7284  recriota  7362  lelttr  7510  ltletr  7511  ltnsymd  7540  lensymd  7542  cnegexlem3  7596  cnegex2  7598  addcanad  7605  addcan2ad  7606  negcon1ad  7725  negne0d  7728  negrebd  7729  subeq0d  7738  subne0ad  7741  neg11d  7742  subcand  7771  subcan2d  7772  ltadd2  7834  ltadd2dd  7837  add20  7889  ltnegcon1d  7936  ltnegcon2d  7937  lenegcon1d  7938  lenegcon2d  7939  subled  7959  lesubd  7960  ltsub23d  7961  ltsub13d  7962  ltadd1dd  7967  ltsub1dd  7968  ltsub2dd  7969  leadd1dd  7970  leadd2dd  7971  lesub1dd  7972  lesub2dd  7973  recexre  7989  apreap  7998  ltmul1a  8002  reapmul1  8006  cru  8013  apreim  8014  mulge0  8030  leltap  8035  ltleap  8041  ltapd  8047  ap0gt0  8049  ap0gt0d  8050  subap0d  8051  mulcanapad  8064  mulcanap2ad  8065  eqnegad  8133  diveqap0d  8195  diveqap1d  8196  divap1d  8199  rec11apd  8209  div11apd  8228  recgt0  8239  prodgt0  8241  lemul1a  8247  lemulge12  8256  lt2msq1  8274  lediv12a  8283  recreclt  8289  nn1suc  8369  nnnlt1  8376  nn2ge  8382  nn1gt1  8383  nnrecl  8597  nn0nlt0  8625  elnn0z  8689  elz2  8744  nn0n0n1ge2b  8752  nnm1ge0  8758  nn0ge0div  8759  zextle  8763  suprzclex  8770  nn0ind-raph  8789  zindd  8790  uzneg  8962  eluzadd  8972  eluzsub  8973  uzm1  8974  uz3m2nn  8986  supminfex  9010  nn01to3  9027  ltrec1d  9119  lerec2d  9120  ledivdivd  9124  divge1  9125  ltmul1dd  9154  ltmul2dd  9155  ltdiv1dd  9156  lediv1dd  9157  ltdiv23d  9159  lediv23d  9160  nn0ledivnn  9163  addlelt  9164  xrlelttr  9196  xrltletr  9197  ixxdisj  9246  icoshftf1o  9333  icodisj  9334  lincmb01cmp  9345  iccf1o  9346  uzsubsubfz  9386  fzdisj  9391  fzopth  9399  fznatpl1  9413  fzsuc2  9416  fzp1disj  9417  fzrev2i  9423  uzdisj  9430  fseq1p1m1  9431  fzm1  9437  fzneuz  9438  fzp1nel  9441  fzrevral  9442  fznn0sub2  9460  fz0fzdiffz0  9462  difelfzle  9466  difelfznle  9467  nn0disj  9470  fzonnsub  9501  fzodisj  9510  fzouzdisj  9512  eluzgtdifelfzo  9529  ubmelfzo  9532  fzonn0p1p1  9545  ubmelm1fzo  9558  fzostep1  9569  exfzdc  9572  subfzo0  9574  qtri3or  9575  exbtwnzlemex  9582  rebtwn2z  9587  qbtwnrelemcalc  9588  qbtwnre  9589  qavgle  9591  apbtwnz  9602  flid  9612  flqwordi  9616  flqmulnn0  9627  flhalf  9630  flltdivnn0lt  9632  fldiv4p1lem1div2  9633  intfracq  9648  flqdiv  9649  flqpmodeq  9655  modqmulnn  9670  mulqaddmodid  9692  modqmuladdim  9695  modqmuladdnn0  9696  m1modge3gt1  9699  q2submod  9713  modaddmodup  9715  modqsubdir  9721  modqeqmodmin  9722  modfzo0difsn  9723  uzsinds  9769  monoord2  9803  isermono  9804  iseqf1olemqcl  9812  iseqf1olemnab  9814  iseqf1olemab  9815  iseqf1olemqf1o  9819  iseqf1olemqk  9820  iseqf1olemqsumkj  9824  iseqf1olemqsumk  9825  iseqf1olemqsum  9826  iseqf1olemp  9828  serile  9844  expival  9848  expnegap0  9854  expgt1  9884  ltexp2a  9898  le2sq2  9921  nnlesq  9948  bernneq  9963  expnbnd  9966  expnlbnd  9967  expnlbnd2  9968  expeq0d  9971  sq11d  10008  expcand  10015  nn0opthd  10019  facdiv  10035  faclbnd6  10041  facubnd  10042  facavg  10043  bcval4  10049  bcp1nk  10059  ibcval5  10060  bcpasc  10063  hashennnuni  10076  focdmex  10084  isfinite4im  10090  hashnncl  10093  hashunlem  10101  fiprsshashgt1  10114  hashfzp1  10121  zfz1isolemiso  10133  iseqcoll  10136  cjth  10168  cjdivap  10231  cjne0d  10269  cjap0d  10270  cvg1nlemcxze  10303  cvg1nlemcau  10305  cvg1nlemres  10306  recvguniq  10316  resqrexlemover  10331  resqrexlemdecn  10333  resqrexlemlo  10334  resqrexlemcalc2  10336  resqrexlemcalc3  10337  resqrexlemnmsq  10338  resqrexlemnm  10339  resqrexlemcvg  10340  resqrexlemglsq  10343  resqrexlemga  10344  leabs  10395  absrele  10404  nn0abscl  10406  ltabs  10408  abslt  10409  absle  10410  abstri  10425  amgm2  10439  sqr11d  10494  abs00d  10507  maxabsle  10525  maxabslemlub  10528  maxleastlt  10536  maxltsup  10539  minmax  10547  climi  10561  climge0  10598  climle  10607  climserile  10618  climrecvg1n  10620  fz1f1o  10647  isummolem3  10652  isummolem2a  10653  isummo  10655  zdvdsdc  10684  dvdstr  10700  dvdsadd2b  10710  dvdslelemd  10711  divconjdvds  10717  alzdvds  10722  dvdsext  10723  fzm1ndvds  10724  fzo0dvdseq  10725  zeo3  10735  even2n  10741  mod2eq1n2dvds  10746  nn0ehalf  10770  nnehalf  10771  nno  10773  nn0oddm1d2  10776  divalglemnqt  10787  divalglemex  10789  divalglemeuneg  10790  divalg2  10793  divalgmod  10794  flodddiv4t2lthalf  10804  zsupcllemstep  10808  infssuzex  10812  dvdsbnd  10815  gcdsupex  10816  gcdsupcl  10817  gcddvds  10822  divgcdz  10830  divgcdnn  10833  gcd0id  10837  gcdneg  10840  gcd1  10845  bezoutlemnewy  10852  bezoutlemstep  10853  bezoutlemmo  10862  bezoutlemsup  10865  dfgcd3  10866  bezout  10867  dfgcd2  10870  mulgcd  10872  sqgcd  10885  dvdssqlem  10886  bezoutr1  10889  lcmval  10912  lcmcllem  10916  dvdslcm  10918  lcmgcdlem  10926  lcmdvds  10928  lcmgcdeq  10932  ncoprmgcdne1b  10938  mulgcddvds  10943  rpmulgcd2  10944  qredeu  10946  rpdvds  10948  prmind2  10969  nprm  10972  dvdsnprmd  10974  divgcdodd  10989  isprm6  10993  prmexpb  10997  pw2dvds  11011  pw2dvdseulemle  11012  oddpwdclemdc  11018  sqne2sq  11022  znege1  11023  sqrt2irraplemnn  11024  divnumden  11041  divdenle  11042  qden1elz  11050  nn0sqrtelqelz  11051  hashdvds  11064  crth  11067  phimullem  11068  hashgcdlem  11070  oddennn  11072  nnsf  11325  peano4nninf  11326  nninfalllemn  11328  nninfsellemeq  11336
  Copyright terms: Public domain W3C validator