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  844  mpbi2and  849  bilukdc  1284  equs5or  1708  eqtrd  2069  eleqtrd  2113  neeqtrd  2227  3netr3d  2231  rexlimd2  2425  ceqsalt  2574  vtoclgft  2598  vtoclegft  2619  elrab3t  2691  eueq2dc  2708  sbceq1dd  2764  csbiedf  2881  sseqtrd  2975  3sstr3d  2981  snssd  3500  dfnfc2  3589  breqtrd  3779  3brtr3d  3784  csbexga  3876  reuhypd  4169  elirr  4224  en2lp  4232  finds  4266  iota4  4828  iota4an  4829  funimaexglem  4925  fneu  4946  fco2  5000  fssres2  5010  fresin  5011  feu  5015  f1orescnv  5085  resdif  5091  funcocnv2  5094  f1oprg  5111  fvelrnb  5164  fimacnv  5239  f1oresrab  5272  fsn2  5280  xpsng  5281  fnressn  5292  fsnunf  5305  foeqcnvco  5373  isores1  5397  isoini2  5401  riota5f  5435  riotass2  5437  riotass  5438  ovmpt2dxf  5568  elopabi  5763  cnvf1o  5788  smores3  5849  tfrlemisucaccv  5880  nnsucsssuc  6010  erref  6062  iserd  6068  swoer  6070  swoord1  6071  swoord2  6072  erth  6086  erthi  6088  eroveu  6133  fndmeng  6225  dfplpq2  6338  ltanqi  6386  ltmnqi  6387  ltaddnq  6390  subhalfnqq  6397  ltbtwnnqq  6398  archnqq  6400  prarloclemarch2  6402  enq0sym  6414  enq0ref  6415  enq0tr  6416  nqnq0pi  6420  nnnq0lem1  6428  distrnq0  6441  prarloclemlt  6475  prarloclemn  6481  prarloclemcalc  6484  genplt2i  6492  addnqprllem  6509  addnqprulem  6510  addlocprlemgt  6516  appdivnq  6543  prmuloc2  6547  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemru  6585  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemladdfu  6625  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  prsrlem1  6650  addgt0sr  6683  lelttr  6883  ltletr  6884  ltnsymd  6913  cnegexlem3  6965  cnegex2  6967  addcanad  6974  addcan2ad  6975  negcon1ad  7093  negne0d  7096  negrebd  7097  subeq0d  7106  subne0ad  7109  neg11d  7110  subcand  7139  subcan2d  7140  ltadd2  7192  ltadd2dd  7195  add20  7244  ltnegcon1d  7291  ltnegcon2d  7292  lenegcon1d  7293  lenegcon2d  7294  subled  7314  lesubd  7315  ltsub23d  7316  ltsub13d  7317  ltadd1dd  7322  ltsub1dd  7323  ltsub2dd  7324  leadd1dd  7325  leadd2dd  7326  lesub1dd  7327  lesub2dd  7328  recexre  7342  apreap  7351  ltmul1a  7355  reapmul1  7359  cru  7366  apreim  7367  mulge0  7383  ltleap  7393  mulcanapad  7406  mulcanap2ad  7407  eqnegad  7472  diveqap0d  7534  diveqap1d  7535  divap1d  7538  rec11apd  7548  div11apd  7567  recgt0  7577  prodgt0  7579  lemul1a  7585  lemulge12  7594  lt2msq1  7612  lediv12a  7621  recreclt  7627  nn1suc  7694  nnnlt1  7701  nn2ge  7707  nn1gt1  7708  nnrecl  7935  nn0nlt0  7964  elnn0z  8014  elz2  8068  nn0n0n1ge2b  8076  nnm1ge0  8082  nn0ge0div  8083  zextle  8087  nn0ind-raph  8111  zindd  8112  uzneg  8247  eluzadd  8257  eluzsub  8258  uzm1  8259  uz3m2nn  8271  nn01to3  8308  ltrec1d  8397  lerec2d  8398  ledivdivd  8402  ltmul1dd  8428  ltmul2dd  8429  ltdiv1dd  8430  lediv1dd  8431  ltdiv23d  8433  lediv23d  8434  xrlelttr  8472  xrltletr  8473  ixxdisj  8522  icoshftf1o  8609  icodisj  8610  lincmb01cmp  8621  iccf1o  8622  uzsubsubfz  8661  fzdisj  8666  fzopth  8674  fznatpl1  8688  fzsuc2  8691  fzp1disj  8692  fzrev2i  8698  uzdisj  8705  fseq1p1m1  8706  fzm1  8712  fzneuz  8713  fzp1nel  8716  fzrevral  8717  elfz0addOLD  8730  fznn0sub2  8735  fz0fzdiffz0  8737  difelfzle  8742  difelfznle  8743  nn0disj  8745  fzonnsub  8775  fzodisj  8784  fzouzdisj  8786  eluzgtdifelfzo  8803  ubmelfzo  8806  fzonn0p1p1  8819  ubmelm1fzo  8832  fzostep1  8843  expival  8891  expnegap0  8897  expgt1  8927  ltexp2a  8940  le2sq2  8962  nnlesq  8989  bernneq  9002  expnbnd  9005  expnlbnd  9006  expnlbnd2  9007  expeq0d  9010  sq11d  9046  cjth  9054  cjdivap  9117  cjne0d  9155  nn0abscl  9209
  Copyright terms: Public domain W3C validator