ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbird 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  6417  nqnq0  6424  addcmpblnq0  6426  mulcanenq0ec  6428  nnnq0lem1  6429  nqpnq0nq  6436  nq0m0r  6439  nq02m  6448  prarloclemlt  6476  prarloclemcalc  6485  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  prmuloclemcalc  6546  mullocprlem  6551  1idprl  6566  1idpru  6567  ltaddpr  6571  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemdisj  6580  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  addcanprg  6590  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlem1  6631  cauappcvgprlem2  6632  caucvgprlemnkj  6637  caucvgprlemopl  6640  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlem2  6651  prsrlem1  6670  0idsr  6695  1idsr  6696  recexgt0sr  6701  archsr  6708  pitonnlem1p1  6742  pitonn  6744  leid  6899  readdcan  6950  addneintrd  6996  addneintr2d  6997  pncan  7014  subsub2  7035  subsub4  7040  negned  7115  subne0d  7127  subneintrd  7162  subneintr2d  7164  subeq0bd  7173  subdi  7178  gt0add  7357  rimul  7369  rereim  7370  ltmul1a  7375  apreim  7387  apirr  7389  mulap0r  7399  msqge0  7400  mulge0  7403  gt0ap0  7408  recexaplem2  7415  mulap0bad  7422  mulap0bbd  7423  divrecap  7449  div0ap  7461  div1  7462  recrecap  7467  divdivdivap  7471  ddcanap  7484  rerecclap  7488  div2negap  7493  recgt0  7597  prodgt0  7599  lemul1a  7605  recp1lt1  7646  squeeze0  7651  peano2nn  7707  arch  7954  peano2z  8057  peano2zm  8059  ztri3or  8064  nn0n0n1ge2  8087  zextle  8107  gtndiv  8111  nn0ind-raph  8131  uzid  8263  uzneg  8267  uztric  8270  uz11  8271  eluzp1l  8273  qdivcl  8352  irrmul  8356  rpnegap  8390  ltpnf  8472  mnflt  8474  pnfge  8480  mnfle  8483  xrlttr  8486  xrltso  8487  xrlttri3  8488  xrleid  8490  iccf1o  8642  fztri3or  8673  fznlem  8675  fzn  8676  fzsplit2  8684  fznatpl1  8708  uzsplit  8724  fseq1p1m1  8726  fzm1  8732  fznn0sub2  8755  difelfznle  8763  1fv  8766  fzospliti  8802  fzouzsplit  8805  eluzgtdifelfzo  8823  frecuzrdgfn  8879  expivallem  8910  expival  8911  expp1  8916  expcllem  8920  ltexp2a  8960  leexp2a  8961  cjth  9074  cjmulrcl  9115  reim0bd  9172  rerebd  9173  cjrebd  9174  bj-sels  9369  bj-nnelon  9419
  Copyright terms: Public domain W3C validator