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  621  mpbir2and  850  pm3.12dc  864  mpbir3and  1086  pm5.15dc  1277  eqeltrd  2111  eqnetrd  2223  3netr4d  2232  sbcne12g  2862  eqsstrd  2973  3sstr4d  2982  eqbrtrd  3775  3brtr4d  3785  snelpwi  3939  prelpwi  3941  pwel  3945  ordelon  4086  onin  4089  elelsuc  4112  suceloni  4193  sucelon  4195  sosng  4356  relssdv  4375  eqbrrdv  4380  eqrelrdv2  4382  breldmg  4484  iss  4597  xpimasn  4712  elxp4  4751  elxp5  4752  funssres  4885  sefvex  5139  fvun1  5182  eqfnfvd  5211  fvimacnvi  5224  fvimacnv  5225  fvelrn  5241  fmpt2d  5270  fmptco  5273  fsn  5278  ftpg  5290  fconst2g  5319  funfvima3  5335  foeqcnvco  5373  f1eqcocnv  5374  fliftfun  5379  fliftfund  5380  fliftval  5383  riota5f  5435  f1ofveu  5443  f1ocnvd  5644  f1opw2  5648  fnofval  5663  off  5666  offval2  5668  ofrfval2  5669  caofref  5674  caofinvl  5675  elxp6  5738  cnvf1olem  5787  f2ndf  5789  tposf12  5825  smores2  5850  tfrlemisucaccv  5880  tfrlemibfn  5883  tfri3  5894  frecsuclemdm  5927  nnsucsssuc  6010  ersym  6054  ertr  6057  swoer  6070  erth  6086  riinerm  6115  qliftfund  6125  eroprf  6135  ecopoverg  6143  th3qlem1  6144  f1dom2g  6172  dom3d  6190  fopwdom  6246  ltsopi  6304  pitri3or  6306  ltdcpi  6307  indpi  6326  enqdc  6345  enqdc1  6346  addcmpblnq  6351  mulcanenq  6369  recrecnq  6378  nqtri3or  6380  ltdcnq  6381  ltsonq  6382  ltaddnq  6390  subhalfnqq  6397  archnqq  6400  prarloclemarch2  6402  enq0tr  6416  nqnq0  6423  addcmpblnq0  6425  mulcanenq0ec  6427  nnnq0lem1  6428  nqpnq0nq  6435  nq0m0r  6438  nq02m  6447  prarloclemlt  6475  prarloclemcalc  6484  addlocpr  6518  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  prmuloclemcalc  6545  mullocprlem  6550  1idprl  6565  1idpru  6566  ltaddpr  6570  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemdisj  6579  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  addcanprg  6589  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlem1  6630  cauappcvgprlem2  6631  prsrlem1  6650  0idsr  6675  1idsr  6676  recexgt0sr  6681  archsr  6688  pitonnlem1p1  6722  pitonn  6724  leid  6879  readdcan  6930  addneintrd  6976  addneintr2d  6977  pncan  6994  subsub2  7015  subsub4  7020  negned  7095  subne0d  7107  subneintrd  7142  subneintr2d  7144  subeq0bd  7153  subdi  7158  gt0add  7337  rimul  7349  rereim  7350  ltmul1a  7355  apreim  7367  apirr  7369  mulap0r  7379  msqge0  7380  mulge0  7383  gt0ap0  7388  recexaplem2  7395  mulap0bad  7402  mulap0bbd  7403  divrecap  7429  div0ap  7441  div1  7442  recrecap  7447  divdivdivap  7451  ddcanap  7464  rerecclap  7468  div2negap  7473  recgt0  7577  prodgt0  7579  lemul1a  7585  recp1lt1  7626  squeeze0  7631  peano2nn  7687  arch  7934  peano2z  8037  peano2zm  8039  ztri3or  8044  nn0n0n1ge2  8067  zextle  8087  gtndiv  8091  nn0ind-raph  8111  uzid  8243  uzneg  8247  uztric  8250  uz11  8251  eluzp1l  8253  qdivcl  8332  irrmul  8336  rpnegap  8370  ltpnf  8452  mnflt  8454  pnfge  8460  mnfle  8463  xrlttr  8466  xrltso  8467  xrlttri3  8468  xrleid  8470  iccf1o  8622  fztri3or  8653  fznlem  8655  fzn  8656  fzsplit2  8664  fznatpl1  8688  uzsplit  8704  fseq1p1m1  8706  fzm1  8712  fznn0sub2  8735  difelfznle  8743  1fv  8746  fzospliti  8782  fzouzsplit  8785  eluzgtdifelfzo  8803  frecuzrdgfn  8859  expivallem  8890  expival  8891  expp1  8896  expcllem  8900  ltexp2a  8940  leexp2a  8941  cjth  9054  cjmulrcl  9095  reim0bd  9152  rerebd  9153  cjrebd  9154  bj-sels  9345
  Copyright terms: Public domain W3C validator