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

Theorem mpbird 165
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbird.min (𝜑𝜒)
mpbird.maj (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mpbird (𝜑𝜓)

Proof of Theorem mpbird
StepHypRef Expression
1 mpbird.min . 2 (𝜑𝜒)
2 mpbird.maj . . 3 (𝜑 → (𝜓𝜒))
32biimprd 156 . 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  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbiri  166  pm5.19  655  mpbir2and  886  pm3.12dc  900  mpbir3and  1122  pm5.15dc  1321  eqeltrd  2156  eqnetrd  2270  3netr4d  2279  sbcne12g  2925  eqsstrd  3034  3sstr4d  3043  eqbrtrd  3813  3brtr4d  3823  snelpwi  3975  prelpwi  3977  pwel  3981  ordelon  4146  onin  4149  elelsuc  4172  suceloni  4253  sucelon  4255  onintonm  4269  sosng  4439  relssdv  4458  eqbrrdv  4463  eqrelrdv2  4465  relsnopg  4470  breldmg  4569  iss  4684  xpimasn  4799  elxp4  4838  elxp5  4839  funssres  4972  sefvex  5227  fvun1  5271  eqfnfvd  5300  fvimacnvi  5313  fvimacnv  5314  fvelrn  5330  fmpt2d  5359  fmptco  5362  fsn  5367  ftpg  5379  fconst2g  5408  funfvima3  5424  foeqcnvco  5461  f1eqcocnv  5462  fliftfun  5467  fliftfund  5468  fliftval  5471  riota5f  5523  f1ofveu  5531  f1ocnvd  5733  f1opw2  5737  fnofval  5752  off  5755  offval2  5757  ofrfval2  5758  caofref  5763  caofinvl  5764  elxp6  5827  cnvf1olem  5876  f2ndf  5878  f1od2  5887  tposf12  5918  smores2  5943  tfrlemisucaccv  5974  tfrlemibfn  5977  tfr1onlemsucaccv  5990  tfr1onlembfn  5993  tfrcllemsucaccv  6003  tfrcllembfn  6006  tfrcl  6013  tfri3  6016  frecabcl  6048  nnsucsssuc  6136  ersym  6184  ertr  6187  swoer  6200  erth  6216  riinerm  6245  qliftfund  6255  eroprf  6265  ecopoverg  6273  th3qlem1  6274  f1dom2g  6303  dom3d  6321  fopwdom  6380  nndomo  6399  dif1en  6414  findcard2  6423  findcard2s  6424  diffisn  6427  fientri3  6435  f1dmvrnfibi  6452  supelti  6474  supsnti  6477  cnvinfex  6490  ordiso2  6505  isnumi  6510  ltsopi  6572  pitri3or  6574  ltdcpi  6575  indpi  6594  enqdc  6613  enqdc1  6614  addcmpblnq  6619  mulcanenq  6637  recrecnq  6646  nqtri3or  6648  ltdcnq  6649  ltsonq  6650  ltaddnq  6659  subhalfnqq  6666  archnqq  6669  prarloclemarch2  6671  enq0tr  6686  nqnq0  6693  addcmpblnq0  6695  mulcanenq0ec  6697  nnnq0lem1  6698  nqpnq0nq  6705  nq0m0r  6708  nq02m  6717  prarloclemlt  6745  prarloclemcalc  6754  addlocpr  6788  nqprl  6803  nqpru  6804  addnqprlemrl  6809  addnqprlemru  6810  prmuloclemcalc  6817  mullocprlem  6822  mulnqprlemrl  6825  mulnqprlemru  6826  1idprl  6842  1idpru  6843  ltaddpr  6849  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemdisj  6858  ltexprlemrl  6862  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  addcanprg  6868  prplnqu  6872  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  aptiprleml  6891  aptiprlemu  6892  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlem1  6911  cauappcvgprlem2  6912  caucvgprlemnkj  6918  caucvgprlemopl  6921  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlem2  6932  caucvgprprlemnkltj  6941  caucvgprprlemopl  6949  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemaddq  6960  caucvgprprlem2  6962  prsrlem1  6981  0idsr  7006  1idsr  7007  recexgt0sr  7012  archsr  7020  prsradd  7024  caucvgsrlemcau  7031  caucvgsrlembound  7032  caucvgsrlemoffgt1  7037  pitonnlem1p1  7076  pitonn  7078  pitoregt0  7079  peano2nnnn  7083  recidpirq  7088  axcaucvglemval  7125  leid  7262  nltled  7297  readdcan  7315  addneintrd  7363  addneintr2d  7364  pncan  7381  subsub2  7403  subsub4  7408  negned  7483  subne0d  7495  subneintrd  7530  subneintr2d  7532  subeq0bd  7550  subdi  7556  gt0add  7740  rimul  7752  rereim  7753  ltmul1a  7758  apreim  7770  apirr  7772  mulap0r  7782  msqge0  7783  mulge0  7786  gt0ap0  7792  ltap  7798  recexaplem2  7809  mulap0bad  7816  mulap0bbd  7817  divrecap  7843  div0ap  7857  div1  7858  recrecap  7864  divdivdivap  7868  ddcanap  7881  rerecclap  7885  div2negap  7890  recgt0  7995  prodgt0  7997  lemul1a  8003  recp1lt1  8044  squeeze0  8049  peano2nn  8118  div4p1lem1div2  8351  arch  8352  peano2z  8468  peano2zm  8470  ztri3or  8475  nn0n0n1ge2  8499  zextle  8519  gtndiv  8523  suprzclex  8526  nn0ind-raph  8545  uzid  8714  uzneg  8718  uztric  8721  uz11  8722  eluzp1l  8724  qdivcl  8809  irrmul  8813  rpnegap  8847  ledivge1le  8884  nn0ledivnn  8919  ltpnf  8932  mnflt  8934  pnfge  8940  mnfle  8943  xrlttr  8946  xrltso  8947  xrlttri3  8948  xrleid  8950  iccf1o  9102  fztri3or  9134  fznlem  9136  fzn  9137  fzsplit2  9145  fznatpl1  9169  uzsplit  9185  fseq1p1m1  9187  fzm1  9193  fznn0sub2  9216  difelfznle  9223  1fv  9226  fzospliti  9262  fzouzsplit  9265  eluzgtdifelfzo  9283  exfzdc  9326  subfzo0  9328  exbtwnz  9337  qbtwnrelemcalc  9342  flqlelt  9358  qfraclt1  9362  qfracge0  9363  flqltnz  9369  btwnzge0  9382  flhalf  9384  ceiqle  9395  intfracq  9402  mulqmod0  9412  modqge0  9414  modqlt  9415  modqid  9431  modqid0  9432  m1modge3gt1  9453  modqltm1p1mod  9458  q2txmodxeq0  9466  modaddmodlo  9470  modsumfzodifsn  9478  addmodlteq  9480  frecuzrdgtcl  9494  frecuzrdgtclt  9503  uzsinds  9518  iseqfclt  9536  iseqoveq  9540  monoord2  9552  iseqid3  9561  serile  9571  expivallem  9574  expival  9575  expp1  9580  expcllem  9584  ltexp2a  9625  leexp2a  9626  faclbnd  9765  faclbnd2  9766  faclbnd3  9767  ibcval5  9787  bcpasc  9790  sizeennn  9804  sizeeqf1oi  9812  sizesng  9822  sizefn  9824  sizeun  9829  shftfn  9850  cjth  9871  cjmulrcl  9912  reim0bd  9969  rerebd  9970  cjrebd  9971  caucvgre  10005  cvg1nlemcxze  10006  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemover  10034  resqrexlemdec  10035  resqrexlemgt0  10044  resqrexlemoverl  10045  resqrexlemglsq  10046  rersqrtthlem  10054  sqrtgt0  10058  leabs  10098  absexpzap  10104  absle  10113  recvalap  10121  abstri  10128  abs2dif  10130  amgm2  10142  absne0d  10211  maxleim  10229  maxabslemab  10230  maxabslemlub  10231  maxltsup  10242  fimaxre2  10247  minmax  10250  climconst  10267  climuni  10270  2clim  10278  climcn1  10285  climcn2  10286  climge0  10301  climle  10310  climsqz  10311  climsqz2  10312  serif0  10327  dvdsval2  10343  dvdsdc  10348  dvds0lem  10350  zdvdsdc  10361  dvdscmulr  10369  dvdsmulcr  10370  dvdslelemd  10388  divconjdvds  10394  dvdsext  10400  fzm1ndvds  10401  dvdsmod  10407  oexpneg  10421  2tp1odd  10428  mulsucdiv2z  10429  2teven  10431  zeo5  10432  opeo  10441  omeo  10442  nn0ob  10452  divalglemnqt  10464  zsupcllemstep  10485  zsupcl  10487  zssinfcl  10488  infssuzex  10489  infssuzcldc  10491  gcddvds  10499  dvdslegcd  10500  gcdneg  10517  bezoutlemnewy  10529  bezoutlemstep  10530  bezoutlema  10532  bezoutlemb  10533  bezoutlemmo  10539  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  bezout  10544  dfgcd2  10547  lcmcllem  10593  lcmneg  10600  lcmgcdlem  10603  lcmdvds  10605  lcmid  10606  3lcm2e6woprm  10612  6lcm4e12  10613  ncoprmgcdne1b  10615  mulgcddvds  10620  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  isprm2lem  10642  prmind2  10646  dvdsnprmd  10651  prm2orodd  10652  sqnprm  10661  rpexp  10676  sqrt2irrlem  10684  oddpwdclemdc  10695  sqrt2irraplemnn  10701  znnen  10709  bj-sels  10863  bj-nnelon  10912
  Copyright terms: Public domain W3C validator