ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbid Unicode 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  6415  enq0ref  6416  enq0tr  6417  nqnq0pi  6421  nnnq0lem1  6429  distrnq0  6442  prarloclemlt  6476  prarloclemn  6482  prarloclemcalc  6485  genplt2i  6493  addnqprllem  6510  addnqprulem  6511  addlocprlemgt  6517  appdivnq  6544  prmuloc2  6548  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemru  6586  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemladdfu  6626  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  archrecnq  6635  caucvgprlemk  6636  caucvgprlemnbj  6638  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  prsrlem1  6670  addgt0sr  6703  lelttr  6903  ltletr  6904  ltnsymd  6933  cnegexlem3  6985  cnegex2  6987  addcanad  6994  addcan2ad  6995  negcon1ad  7113  negne0d  7116  negrebd  7117  subeq0d  7126  subne0ad  7129  neg11d  7130  subcand  7159  subcan2d  7160  ltadd2  7212  ltadd2dd  7215  add20  7264  ltnegcon1d  7311  ltnegcon2d  7312  lenegcon1d  7313  lenegcon2d  7314  subled  7334  lesubd  7335  ltsub23d  7336  ltsub13d  7337  ltadd1dd  7342  ltsub1dd  7343  ltsub2dd  7344  leadd1dd  7345  leadd2dd  7346  lesub1dd  7347  lesub2dd  7348  recexre  7362  apreap  7371  ltmul1a  7375  reapmul1  7379  cru  7386  apreim  7387  mulge0  7403  ltleap  7413  mulcanapad  7426  mulcanap2ad  7427  eqnegad  7492  diveqap0d  7554  diveqap1d  7555  divap1d  7558  rec11apd  7568  div11apd  7587  recgt0  7597  prodgt0  7599  lemul1a  7605  lemulge12  7614  lt2msq1  7632  lediv12a  7641  recreclt  7647  nn1suc  7714  nnnlt1  7721  nn2ge  7727  nn1gt1  7728  nnrecl  7955  nn0nlt0  7984  elnn0z  8034  elz2  8088  nn0n0n1ge2b  8096  nnm1ge0  8102  nn0ge0div  8103  zextle  8107  nn0ind-raph  8131  zindd  8132  uzneg  8267  eluzadd  8277  eluzsub  8278  uzm1  8279  uz3m2nn  8291  nn01to3  8328  ltrec1d  8417  lerec2d  8418  ledivdivd  8422  ltmul1dd  8448  ltmul2dd  8449  ltdiv1dd  8450  lediv1dd  8451  ltdiv23d  8453  lediv23d  8454  xrlelttr  8492  xrltletr  8493  ixxdisj  8542  icoshftf1o  8629  icodisj  8630  lincmb01cmp  8641  iccf1o  8642  uzsubsubfz  8681  fzdisj  8686  fzopth  8694  fznatpl1  8708  fzsuc2  8711  fzp1disj  8712  fzrev2i  8718  uzdisj  8725  fseq1p1m1  8726  fzm1  8732  fzneuz  8733  fzp1nel  8736  fzrevral  8737  elfz0addOLD  8750  fznn0sub2  8755  fz0fzdiffz0  8757  difelfzle  8762  difelfznle  8763  nn0disj  8765  fzonnsub  8795  fzodisj  8804  fzouzdisj  8806  eluzgtdifelfzo  8823  ubmelfzo  8826  fzonn0p1p1  8839  ubmelm1fzo  8852  fzostep1  8863  expival  8911  expnegap0  8917  expgt1  8947  ltexp2a  8960  le2sq2  8982  nnlesq  9009  bernneq  9022  expnbnd  9025  expnlbnd  9026  expnlbnd2  9027  expeq0d  9030  sq11d  9066  cjth  9074  cjdivap  9137  cjne0d  9175  nn0abscl  9229
  Copyright terms: Public domain W3C validator