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

Theorem simp3 983
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp3 ((𝜑𝜓𝜒) → 𝜒)

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 980 . 2 ((𝜑𝜓𝜒) → (𝜓𝜒))
21simprd 113 1 ((𝜑𝜓𝜒) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  simpl3  986  simpr3  989  simp3i  992  simp3d  995  simp13  1013  simp23  1016  simp33  1019  3anibar  1149  3ianorr  1287  stoic4a  1408  stoic4b  1409  mob2  2864  sotri2  4936  sotri3  4937  feq123  5264  resasplitss  5302  sefvex  5442  ftpg  5604  fsnunf  5620  fnfvima  5652  cocan1  5688  cocan2  5689  f1oiso2  5728  riotass  5757  moriotass  5758  ovmpox  5899  ovmpoga  5900  caovimo  5964  ofrval  5992  dfsmo2  6184  tfr1onlembfn  6241  tfrcllembfn  6254  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  nnsucsssuc  6388  f1oen2g  6649  f1dom2g  6650  xpdom3m  6728  mapxpen  6742  diffifi  6788  unfidisj  6810  undifdc  6812  ssfidc  6823  sbthlemi9  6853  ctssdc  6998  endjudisj  7071  djuassen  7078  xpdjuen  7079  mulcanenq  7205  ltanqg  7220  addnnnq0  7269  nnanq0  7278  prltlu  7307  distrprg  7408  ltexprlemm  7420  recexprlem1ssl  7453  recexprlem1ssu  7454  addsrpr  7565  mulsrpr  7566  mulasssrg  7578  recexgt0sr  7593  ltpsrprg  7623  axmulass  7693  axpre-ltadd  7706  ltxrlt  7842  subadd2  7978  addsubass  7984  nppcan  7996  nppcan3  7998  subcan2  7999  subsub2  8002  subsub4  8007  pnpcan  8013  pnncan  8015  subcan  8029  subdi  8159  ltadd1  8203  leadd1  8204  leadd2  8205  ltsubadd  8206  ltsubadd2  8207  lesubadd  8208  lesubadd2  8209  ltaddsub  8210  leaddsub  8212  lesub1  8230  lesub2  8231  ltsub1  8232  ltsub2  8233  ltaddsublt  8345  gt0add  8347  reapadd1  8370  remulext1  8373  remulext2  8374  apadd2  8383  mulext2  8387  mulap0r  8389  leltap  8399  ltap  8407  apsub1  8416  divap0b  8455  divmulasscomap  8468  divcanap5  8486  dmdcanap  8494  redivclap  8503  div2negap  8507  lt2msq1  8655  ltdiv2  8657  nndivtr  8774  gtndiv  9158  eluzsub  9367  nn01to3  9421  qdivcl  9447  irrmul  9451  rpgecl  9482  divge1  9522  xaddass  9664  xltadd1  9671  ubioog  9709  ubioc1  9724  lbico1  9725  iccleub  9726  lbicc2  9779  ubicc2  9780  icoshftf1o  9786  fzen  9835  elfz1b  9882  uznfz  9895  elfzo0  9971  elfzo0z  9973  ubmelfzo  9989  fzonn0p1p1  10002  ubmelm1fzo  10015  qbtwnre  10046  flqwordi  10073  flltdivnn0lt  10089  ceiqle  10098  modqval  10109  modqvalr  10110  modqcl  10111  flqpmodeq  10112  modq0  10114  mulqmod0  10115  negqmod0  10116  modqge0  10117  modqlt  10118  modqdiffl  10120  modqdifz  10121  modqmulnn  10127  modqvalp1  10128  modqabs2  10143  modqmuladdnn0  10153  qnegmod  10154  addmodid  10157  modqeqmodmin  10179  modfzo0difsn  10180  addmodlteq  10183  frec2uzf1od  10191  expnegap0  10313  expgt1  10343  exprecap  10346  expaddzaplem  10348  expaddzap  10349  expmulzap  10351  mulbinom2  10420  expnbnd  10427  fihashss  10574  fimaxq  10585  seq3coll  10597  shftfibg  10604  redivap  10658  imdivap  10665  cjdivap  10693  maxleast  10997  lemininf  11017  ltmininf  11018  bdtrilem  11022  bdtri  11023  xrmaxaddlem  11041  xrmaxadd  11042  xrmineqinf  11050  xrltmininf  11051  xrminltinf  11053  xrminadd  11056  climuni  11074  reccn2ap  11094  isumz  11170  fsumsplitsnun  11200  geoisum1c  11301  prodfap0  11326  cos12dec  11485  summodnegmod  11535  dvdsmultr2  11544  mulmoddvds  11572  divalglemeuneg  11631  gcdaddm  11683  gcdass  11714  mulgcd  11715  gcddiv  11718  lcmass  11777  mulgcddvds  11786  qredeq  11788  congr  11792  divgcdcoprmex  11794  cncongr1  11795  cncongr2  11796  prmexpb  11840  rpexp  11842  unennn  11921  fvsetsid  12007  ressid2  12032  ressval2  12033  rngmulrg  12091  basgen  12263  2basgeng  12265  ntrss  12302  neiss  12333  opnneiss  12341  restco  12357  restabs  12358  cnprcl2k  12389  cnpf2  12390  lmconst  12399  cnpnei  12402  cnptoprest  12422  cnmpt2t  12476  psmetsym  12512  psmetge0  12514  xmetge0  12548  xmetsym  12551  blvalps  12571  blval  12572  ssblps  12608  ssbl  12609  blpnfctr  12622  xmssym  12652  bdxmet  12684  metcnp3  12694  dvfvalap  12833  dvid  12845  dvcnp2cntop  12846  ptolemy  12927
  Copyright terms: Public domain W3C validator