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

Theorem mpbid 135
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
mpbid.min (φψ)
mpbid.maj (φ → (ψχ))
Assertion
Ref Expression
mpbid (φχ)

Proof of Theorem mpbid
StepHypRef Expression
1 mpbid.min . 2 (φψ)
2 mpbid.maj . . 3 (φ → (ψχ))
32biimpd 132 . 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
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbii  136  annimdc  831  mpbi2and  836  bilukdc  1268  equs5or  1689  eqtrd  2050  eleqtrd  2094  neeqtrd  2207  3netr3d  2211  rexlimd2  2405  ceqsalt  2553  vtoclgft  2577  vtoclegft  2598  elrab3t  2670  eueq2dc  2687  sbceq1dd  2743  csbiedf  2860  sseqtrd  2954  3sstr3d  2960  snssd  3479  dfnfc2  3568  breqtrd  3758  3brtr3d  3763  csbexgOLD  3855  reuhypd  4149  elirr  4204  en2lp  4212  finds  4246  iota4  4808  iota4an  4809  funimaexglem  4904  fneu  4925  fco2  4978  fssres2  4988  fresin  4989  feu  4993  f1orescnv  5063  resdif  5069  funcocnv2  5072  f1oprg  5089  fvelrnb  5142  fimacnv  5217  f1oresrab  5250  fsn2  5258  xpsng  5259  fnressn  5270  fsnunf  5283  foeqcnvco  5351  isores1  5375  isoini2  5379  riota5f  5412  riotass2  5414  riotass  5415  ovmpt2dxf  5545  elopabi  5740  cnvf1o  5765  smores3  5826  tfrlemisucaccv  5856  nnsucsssuc  5982  erref  6033  iserd  6039  swoer  6041  swoord1  6042  swoord2  6043  erth  6057  erthi  6059  eroveu  6104  dfplpq2  6207  ltanqi  6255  ltmnqi  6256  ltaddnq  6259  subhalfnqq  6265  ltbtwnnqq  6266  archnqq  6268  prarloclemarch2  6270  enq0sym  6281  enq0ref  6282  enq0tr  6283  nqnq0pi  6287  nnnq0lem1  6295  distrnq0  6308  prarloclemlt  6341  prarloclemn  6347  prarloclemcalc  6350  genplt2i  6358  addnqprllem  6376  addnqprulem  6377  addlocprlemgt  6383  appdivnq  6401  prmuloc2  6405  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemru  6443  prsrlem1  6483  addgt0sr  6515  lelttr  6698  ltletr  6699  ltnsymd  6723  cnegexlem3  6775  cnegex2  6777  addcanad  6784  addcan2ad  6785  negcon1ad  6903  negne0d  6906  negrebd  6907  subeq0d  6916  subne0ad  6919  neg11d  6920  subcand  6949  subcan2d  6950  ltadd2  7002  ltadd2dd  7005  ltnegcon1d  7097  ltnegcon2d  7098  lenegcon1d  7099  lenegcon2d  7100  subled  7120  lesubd  7121  ltsub23d  7122  ltsub13d  7123  ltadd1dd  7128  ltsub1dd  7129  ltsub2dd  7130  leadd1dd  7131  leadd2dd  7132  lesub1dd  7133  lesub2dd  7134
  Copyright terms: Public domain W3C validator