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  3499  dfnfc2  3588  breqtrd  3778  3brtr3d  3783  csbexga  3875  reuhypd  4168  elirr  4223  en2lp  4231  finds  4265  iota4  4827  iota4an  4828  funimaexglem  4923  fneu  4944  fco2  4998  fssres2  5008  fresin  5009  feu  5013  f1orescnv  5083  resdif  5089  funcocnv2  5092  f1oprg  5109  fvelrnb  5162  fimacnv  5237  f1oresrab  5270  fsn2  5278  xpsng  5279  fnressn  5290  fsnunf  5303  foeqcnvco  5371  isores1  5395  isoini2  5399  riota5f  5432  riotass2  5434  riotass  5435  ovmpt2dxf  5565  elopabi  5760  cnvf1o  5785  smores3  5846  tfrlemisucaccv  5877  nnsucsssuc  6003  erref  6055  iserd  6061  swoer  6063  swoord1  6064  swoord2  6065  erth  6079  erthi  6081  eroveu  6126  fndmeng  6218  dfplpq2  6331  ltanqi  6379  ltmnqi  6380  ltaddnq  6383  subhalfnqq  6390  ltbtwnnqq  6391  archnqq  6393  prarloclemarch2  6395  enq0sym  6407  enq0ref  6408  enq0tr  6409  nqnq0pi  6413  nnnq0lem1  6421  distrnq0  6434  prarloclemlt  6468  prarloclemn  6474  prarloclemcalc  6477  genplt2i  6485  addnqprllem  6503  addnqprulem  6504  addlocprlemgt  6510  appdivnq  6534  prmuloc2  6538  ltexprlemopl  6565  ltexprlemopu  6567  ltexprlemru  6576  prsrlem1  6622  addgt0sr  6655  lelttr  6855  ltletr  6856  ltnsymd  6885  cnegexlem3  6937  cnegex2  6939  addcanad  6946  addcan2ad  6947  negcon1ad  7065  negne0d  7068  negrebd  7069  subeq0d  7078  subne0ad  7081  neg11d  7082  subcand  7111  subcan2d  7112  ltadd2  7164  ltadd2dd  7167  add20  7216  ltnegcon1d  7263  ltnegcon2d  7264  lenegcon1d  7265  lenegcon2d  7266  subled  7286  lesubd  7287  ltsub23d  7288  ltsub13d  7289  ltadd1dd  7294  ltsub1dd  7295  ltsub2dd  7296  leadd1dd  7297  leadd2dd  7298  lesub1dd  7299  lesub2dd  7300  recexre  7314  apreap  7323  ltmul1a  7327  reapmul1  7331  cru  7338  apreim  7339  mulge0  7355  ltleap  7365  mulcanapad  7378  mulcanap2ad  7379  eqnegad  7444  diveqap0d  7506  diveqap1d  7507  divap1d  7510  rec11apd  7520  div11apd  7539  recgt0  7548  prodgt0  7550  lemul1a  7556  lemulge12  7565  lt2msq1  7583  lediv12a  7592  recreclt  7598  nn1suc  7665  nnnlt1  7672  nn2ge  7678  nn1gt1  7679  nnrecl  7905  nn0nlt0  7934  elnn0z  7984  elz2  8038  nn0n0n1ge2b  8045  nnm1ge0  8051  nn0ge0div  8052  zextle  8056  nn0ind-raph  8080  zindd  8081  uzneg  8216  eluzadd  8226  eluzsub  8227  uzm1  8228  uz3m2nn  8240  nn01to3  8277  ltrec1d  8365  lerec2d  8366  ledivdivd  8370  ltmul1dd  8396  ltmul2dd  8397  ltdiv1dd  8398  lediv1dd  8399  ltdiv23d  8401  lediv23d  8402  xrlelttr  8440  xrltletr  8441  ixxdisj  8490  icoshftf1o  8577  icodisj  8578  lincmb01cmp  8589  iccf1o  8590  uzsubsubfz  8627  fzdisj  8632  fzopth  8640  fznatpl1  8654  fzsuc2  8657  fzp1disj  8658  fzrev2i  8664  uzdisj  8671  fseq1p1m1  8672  fzm1  8678  fzneuz  8679  fzp1nel  8682  fzrevral  8683  elfz0addOLD  8696  fznn0sub2  8701  fz0fzdiffz0  8703  difelfzle  8708  difelfznle  8709  nn0disj  8711  fzonnsub  8741  fzodisj  8750  fzouzdisj  8752  eluzgtdifelfzo  8769  ubmelfzo  8772  fzonn0p1p1  8785  ubmelm1fzo  8798  fzostep1  8809
  Copyright terms: Public domain W3C validator