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  6510  addnqprulem  6511  addlocprlemgt  6517  appdivnq  6542  prmuloc2  6546  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemru  6584  prsrlem1  6630  addgt0sr  6663  lelttr  6863  ltletr  6864  ltnsymd  6893  cnegexlem3  6945  cnegex2  6947  addcanad  6954  addcan2ad  6955  negcon1ad  7073  negne0d  7076  negrebd  7077  subeq0d  7086  subne0ad  7089  neg11d  7090  subcand  7119  subcan2d  7120  ltadd2  7172  ltadd2dd  7175  add20  7224  ltnegcon1d  7271  ltnegcon2d  7272  lenegcon1d  7273  lenegcon2d  7274  subled  7294  lesubd  7295  ltsub23d  7296  ltsub13d  7297  ltadd1dd  7302  ltsub1dd  7303  ltsub2dd  7304  leadd1dd  7305  leadd2dd  7306  lesub1dd  7307  lesub2dd  7308  recexre  7322  apreap  7331  ltmul1a  7335  reapmul1  7339  cru  7346  apreim  7347  mulge0  7363  ltleap  7373  mulcanapad  7386  mulcanap2ad  7387  eqnegad  7452  diveqap0d  7514  diveqap1d  7515  divap1d  7518  rec11apd  7528  div11apd  7547  recgt0  7557  prodgt0  7559  lemul1a  7565  lemulge12  7574  lt2msq1  7592  lediv12a  7601  recreclt  7607  nn1suc  7674  nnnlt1  7681  nn2ge  7687  nn1gt1  7688  nnrecl  7915  nn0nlt0  7944  elnn0z  7994  elz2  8048  nn0n0n1ge2b  8056  nnm1ge0  8062  nn0ge0div  8063  zextle  8067  nn0ind-raph  8091  zindd  8092  uzneg  8227  eluzadd  8237  eluzsub  8238  uzm1  8239  uz3m2nn  8251  nn01to3  8288  ltrec1d  8377  lerec2d  8378  ledivdivd  8382  ltmul1dd  8408  ltmul2dd  8409  ltdiv1dd  8410  lediv1dd  8411  ltdiv23d  8413  lediv23d  8414  xrlelttr  8452  xrltletr  8453  ixxdisj  8502  icoshftf1o  8589  icodisj  8590  lincmb01cmp  8601  iccf1o  8602  uzsubsubfz  8641  fzdisj  8646  fzopth  8654  fznatpl1  8668  fzsuc2  8671  fzp1disj  8672  fzrev2i  8678  uzdisj  8685  fseq1p1m1  8686  fzm1  8692  fzneuz  8693  fzp1nel  8696  fzrevral  8697  elfz0addOLD  8710  fznn0sub2  8715  fz0fzdiffz0  8717  difelfzle  8722  difelfznle  8723  nn0disj  8725  fzonnsub  8755  fzodisj  8764  fzouzdisj  8766  eluzgtdifelfzo  8783  ubmelfzo  8786  fzonn0p1p1  8799  ubmelm1fzo  8812  fzostep1  8823  expival  8871  expnegap0  8877  expgt1  8907  ltexp2a  8920  le2sq2  8942  nnlesq  8969  bernneq  8982  expnbnd  8985  expnlbnd  8986  expnlbnd2  8987  expeq0d  8990  sq11d  9026  cjth  9034  cjdivap  9097  cjne0d  9135
  Copyright terms: Public domain W3C validator