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  609  mpbir2and  839  pm3.12dc  853  mpbir3and  1072  pm5.15dc  1263  eqeltrd  2096  eqnetrd  2207  3netr4d  2216  sbcne12g  2845  eqsstrd  2956  3sstr4d  2965  eqbrtrd  3758  3brtr4d  3768  snelpwi  3922  prelpwi  3924  pwel  3928  ordelon  4069  onin  4072  elelsuc  4095  suceloni  4177  sucelon  4179  sosng  4340  relssdv  4359  eqbrrdv  4364  eqrelrdv2  4366  breldmg  4468  iss  4581  xpimasn  4696  elxp4  4735  elxp5  4736  funssres  4868  sefvex  5121  fvun1  5164  eqfnfvd  5193  fvimacnvi  5206  fvimacnv  5207  fvelrn  5223  fmpt2d  5252  fmptco  5255  fsn  5260  ftpg  5272  fconst2g  5301  funfvima3  5317  foeqcnvco  5355  f1eqcocnv  5356  fliftfun  5361  fliftfund  5362  fliftval  5365  riota5f  5416  f1ofveu  5424  f1ocnvd  5625  f1opw2  5629  fnofval  5644  off  5647  offval2  5649  ofrfval2  5650  caofref  5655  caofinvl  5656  elxp6  5719  cnvf1olem  5768  f2ndf  5770  tposf12  5806  smores2  5831  tfrlemisucaccv  5860  tfrlemibfn  5863  tfri3  5875  frecsuclemdm  5904  nnsucsssuc  5986  ersym  6029  ertr  6032  swoer  6045  erth  6061  riinerm  6090  qliftfund  6100  eroprf  6110  ecopoverg  6118  th3qlem1  6119  ltsopi  6180  pitri3or  6182  ltdcpi  6183  enqdc  6220  enqdc1  6221  addcmpblnq  6226  mulcanenq  6244  recrecnq  6253  nqtri3or  6255  ltdcnq  6256  ltsonq  6257  ltaddnq  6265  subhalfnqq  6271  archnqq  6274  prarloclemarch2  6276  enq0tr  6289  nqnq0  6296  addcmpblnq0  6298  mulcanenq0ec  6300  nnnq0lem1  6301  nqpnq0nq  6308  nq0m0r  6311  nq02m  6319  prarloclemlt  6347  prarloclemcalc  6356  addlocpr  6391  prmuloclemcalc  6409  mullocprlem  6414  1idprl  6429  1idpru  6430  ltaddpr  6434  ltexprlemm  6437  ltexprlemopl  6438  ltexprlemopu  6440  ltexprlemdisj  6443  ltexprlemrl  6447  ltexprlemru  6449  addcanprleml  6451  addcanprlemu  6452  addcanprg  6453  recexprlemloc  6465  recexprlem1ssl  6467  recexprlem1ssu  6468  prsrlem1  6489  0idsr  6514  1idsr  6515  recexsrlem  6520  leid  6700  readdcan  6746  addneintrd  6792  addneintr2d  6793  pncan  6810  subsub2  6831  subsub4  6836  negned  6911  subne0d  6923  subneintrd  6958  subneintr2d  6960  subeq0bd  6969  subdi  6974  bj-sels  7284
  Copyright terms: Public domain W3C validator