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  6519  addnqpr1lemrl  6537  addnqpr1lemru  6538  prmuloclemcalc  6544  mullocprlem  6549  1idprl  6564  1idpru  6565  ltaddpr  6569  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemdisj  6578  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  addcanprg  6588  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  aptiprleml  6609  aptiprlemu  6610  archpr  6613  prsrlem1  6630  0idsr  6655  1idsr  6656  recexgt0sr  6661  archsr  6668  pitonnlem1p1  6702  pitonn  6704  leid  6859  readdcan  6910  addneintrd  6956  addneintr2d  6957  pncan  6974  subsub2  6995  subsub4  7000  negned  7075  subne0d  7087  subneintrd  7122  subneintr2d  7124  subeq0bd  7133  subdi  7138  gt0add  7317  rimul  7329  rereim  7330  ltmul1a  7335  apreim  7347  apirr  7349  mulap0r  7359  msqge0  7360  mulge0  7363  gt0ap0  7368  recexaplem2  7375  mulap0bad  7382  mulap0bbd  7383  divrecap  7409  div0ap  7421  div1  7422  recrecap  7427  divdivdivap  7431  ddcanap  7444  rerecclap  7448  div2negap  7453  recgt0  7557  prodgt0  7559  lemul1a  7565  recp1lt1  7606  squeeze0  7611  peano2nn  7667  arch  7914  peano2z  8017  peano2zm  8019  ztri3or  8024  nn0n0n1ge2  8047  zextle  8067  gtndiv  8071  nn0ind-raph  8091  uzid  8223  uzneg  8227  uztric  8230  uz11  8231  eluzp1l  8233  qdivcl  8312  irrmul  8316  rpnegap  8350  ltpnf  8432  mnflt  8434  pnfge  8440  mnfle  8443  xrlttr  8446  xrltso  8447  xrlttri3  8448  xrleid  8450  iccf1o  8602  fztri3or  8633  fznlem  8635  fzn  8636  fzsplit2  8644  fznatpl1  8668  uzsplit  8684  fseq1p1m1  8686  fzm1  8692  fznn0sub2  8715  difelfznle  8723  1fv  8726  fzospliti  8762  fzouzsplit  8765  eluzgtdifelfzo  8783  frecuzrdgfn  8839  expivallem  8870  expival  8871  expp1  8876  expcllem  8880  ltexp2a  8920  leexp2a  8921  cjth  9034  cjmulrcl  9075  reim0bd  9132  rerebd  9133  cjrebd  9134  bj-sels  9299
  Copyright terms: Public domain W3C validator