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

Theorem mpbird 156
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 147 . 2 (φ → (χψ))
41, 3mpd 13 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbiri  157  pm5.19  606  mpbir2and  835  pm3.12dc  849  mpbir3and  1071  pm5.15dc  1261  eqeltrd  2090  eqnetrd  2201  3netr4d  2210  sbcne12g  2839  eqsstrd  2950  3sstr4d  2959  eqbrtrd  3750  3brtr4d  3760  snelpwi  3914  prelpwi  3916  pwel  3920  ordelon  4061  onin  4064  elelsuc  4087  suceloni  4168  sucelon  4170  sosng  4331  relssdv  4350  eqbrrdv  4355  eqrelrdv2  4357  breldmg  4459  iss  4572  xpimasn  4687  elxp4  4726  elxp5  4727  funssres  4859  sefvex  5112  fvun1  5155  eqfnfvd  5184  fvimacnvi  5197  fvimacnv  5198  fvelrn  5214  fmpt2d  5243  fmptco  5246  fsn  5251  ftpg  5263  fconst2g  5292  funfvima3  5308  foeqcnvco  5346  f1eqcocnv  5347  fliftfun  5352  fliftfund  5353  fliftval  5356  riota5f  5407  f1ofveu  5415  f1ocnvd  5616  f1opw2  5620  fnofval  5635  off  5638  offval2  5640  ofrfval2  5641  caofref  5646  caofinvl  5647  elxp6  5710  cnvf1olem  5759  f2ndf  5761  tposf12  5797  smores2  5822  tfrlemisucaccv  5851  tfrlemibfn  5854  tfri3  5866  frecsuclemdm  5895  nnsucsssuc  5977  ersym  6020  ertr  6023  swoer  6036  erth  6052  riinerm  6081  qliftfund  6091  eroprf  6101  ecopoverg  6109  th3qlem1  6110  ltsopi  6169  pitri3or  6171  ltdcpi  6172  enqdc  6209  enqdc1  6210  addcmpblnq  6215  mulcanenq  6233  recrecnq  6242  nqtri3or  6244  ltdcnq  6245  ltsonq  6246  ltaddnq  6254  subhalfnqq  6260  archnqq  6263  prarloclemarch2  6265  enq0tr  6278  nqnq0  6285  addcmpblnq0  6287  mulcanenq0ec  6289  nnnq0lem1  6290  nqpnq0nq  6297  nq0m0r  6300  nq02m  6308  prarloclemlt  6336  prarloclemcalc  6345  addlocpr  6380  prmuloclemcalc  6398  mullocprlem  6403  1idprl  6418  1idpru  6419  ltaddpr  6423  ltexprlemm  6426  ltexprlemopl  6427  ltexprlemopu  6429  ltexprlemdisj  6432  ltexprlemrl  6436  ltexprlemru  6438  addcanprleml  6440  addcanprlemu  6441  addcanprg  6442  recexprlemloc  6455  recexprlem1ssl  6457  recexprlem1ssu  6458  aptiprleml  6463  aptiprlemu  6464  prsrlem1  6483  0idsr  6508  1idsr  6509  recexgt0sr  6514  leid  6705  readdcan  6756  addneintrd  6802  addneintr2d  6803  pncan  6820  subsub2  6841  subsub4  6846  negned  6921  subne0d  6933  subneintrd  6968  subneintr2d  6970  subeq0bd  6979  subdi  6984  gt0add  7163  rimul  7175  rereim  7176  ltmul1a  7181  apreim  7193  apirr  7195  mulap0r  7205  msqge0  7206  mulge0  7209  gt0ap0  7214  recexaplem2  7221  mulap0bad  7228  mulap0bbd  7229  divrecap  7255  div0ap  7267  div1  7268  recrecap  7273  divdivdivap  7277  ddcanap  7290  rerecclap  7294  div2negap  7299  recgt0  7402  prodgt0  7404  lemul1a  7410  recp1lt1  7451  squeeze0  7456  peano2nn  7512  peano2z  7857  peano2zm  7859  ztri3or  7864  zextle  7900  gtndiv  7904  nn0ind-raph  7924  uzid  8055  uzneg  8059  uztric  8062  uz11  8063  eluzp1l  8065  qdivcl  8126  irrmul  8130  rpnegap  8163  ltpnf  8245  mnflt  8247  pnfge  8253  mnfle  8256  xrlttr  8259  xrltso  8260  xrlttri3  8261  xrleid  8263  iccf1o  8415  bj-sels  8551
  Copyright terms: Public domain W3C validator