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

Theorem simp3 966
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp3  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 963 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
21simprd 113 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
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 947
This theorem is referenced by:  simpl3  969  simpr3  972  simp3i  975  simp3d  978  simp13  996  simp23  999  simp33  1002  3anibar  1132  3ianorr  1270  stoic4a  1391  stoic4b  1392  mob2  2835  sotri2  4904  sotri3  4905  feq123  5232  resasplitss  5270  sefvex  5408  ftpg  5570  fsnunf  5586  fnfvima  5618  cocan1  5654  cocan2  5655  f1oiso2  5694  riotass  5723  moriotass  5724  ovmpox  5865  ovmpoga  5866  caovimo  5930  ofrval  5958  dfsmo2  6150  tfr1onlembfn  6207  tfrcllembfn  6220  freccllem  6265  frecfcllem  6267  frecsuclem  6269  frecrdg  6271  nnsucsssuc  6354  f1oen2g  6615  f1dom2g  6616  xpdom3m  6694  mapxpen  6708  diffifi  6754  unfidisj  6776  undifdc  6778  ssfidc  6789  sbthlemi9  6819  ctssdc  6964  endjudisj  7030  djuassen  7037  xpdjuen  7038  mulcanenq  7157  ltanqg  7172  addnnnq0  7221  nnanq0  7230  prltlu  7259  distrprg  7360  ltexprlemm  7372  recexprlem1ssl  7405  recexprlem1ssu  7406  addsrpr  7517  mulsrpr  7518  mulasssrg  7530  recexgt0sr  7545  ltpsrprg  7575  axmulass  7645  axpre-ltadd  7658  ltxrlt  7794  subadd2  7930  addsubass  7936  nppcan  7948  nppcan3  7950  subcan2  7951  subsub2  7954  subsub4  7959  pnpcan  7965  pnncan  7967  subcan  7981  subdi  8111  ltadd1  8155  leadd1  8156  leadd2  8157  ltsubadd  8158  ltsubadd2  8159  lesubadd  8160  lesubadd2  8161  ltaddsub  8162  leaddsub  8164  lesub1  8182  lesub2  8183  ltsub1  8184  ltsub2  8185  ltaddsublt  8296  gt0add  8298  reapadd1  8321  remulext1  8324  remulext2  8325  apadd2  8334  mulext2  8338  mulap0r  8340  leltap  8350  ltap  8357  apsub1  8366  divap0b  8403  divmulasscomap  8416  divcanap5  8434  dmdcanap  8442  redivclap  8451  div2negap  8455  lt2msq1  8600  ltdiv2  8602  nndivtr  8719  gtndiv  9097  eluzsub  9304  nn01to3  9358  qdivcl  9384  irrmul  9388  rpgecl  9418  divge1  9456  xaddass  9592  xltadd1  9599  ubioog  9637  ubioc1  9652  lbico1  9653  iccleub  9654  lbicc2  9707  ubicc2  9708  icoshftf1o  9714  fzen  9763  elfz1b  9810  uznfz  9823  elfzo0  9899  elfzo0z  9901  ubmelfzo  9917  fzonn0p1p1  9930  ubmelm1fzo  9943  qbtwnre  9974  flqwordi  10001  flltdivnn0lt  10017  ceiqle  10026  modqval  10037  modqvalr  10038  modqcl  10039  flqpmodeq  10040  modq0  10042  mulqmod0  10043  negqmod0  10044  modqge0  10045  modqlt  10046  modqdiffl  10048  modqdifz  10049  modqmulnn  10055  modqvalp1  10056  modqabs2  10071  modqmuladdnn0  10081  qnegmod  10082  addmodid  10085  modqeqmodmin  10107  modfzo0difsn  10108  addmodlteq  10111  frec2uzf1od  10119  expnegap0  10241  expgt1  10271  exprecap  10274  expaddzaplem  10276  expaddzap  10277  expmulzap  10279  mulbinom2  10348  expnbnd  10355  fihashss  10502  fimaxq  10513  seq3coll  10525  shftfibg  10532  redivap  10586  imdivap  10593  cjdivap  10621  maxleast  10925  lemininf  10945  ltmininf  10946  bdtrilem  10950  bdtri  10951  xrmaxaddlem  10969  xrmaxadd  10970  xrmineqinf  10978  xrltmininf  10979  xrminltinf  10981  xrminadd  10984  climuni  11002  reccn2ap  11022  isumz  11098  fsumsplitsnun  11128  geoisum1c  11229  summodnegmod  11420  dvdsmultr2  11429  mulmoddvds  11457  divalglemeuneg  11516  gcdaddm  11568  gcdass  11599  mulgcd  11600  gcddiv  11603  lcmass  11662  mulgcddvds  11671  qredeq  11673  congr  11677  divgcdcoprmex  11679  cncongr1  11680  cncongr2  11681  prmexpb  11725  rpexp  11727  unennn  11805  fvsetsid  11888  ressid2  11913  ressval2  11914  rngmulrg  11972  basgen  12144  2basgeng  12146  ntrss  12183  neiss  12214  opnneiss  12222  restco  12238  restabs  12239  cnprcl2k  12270  cnpf2  12271  lmconst  12280  cnpnei  12283  cnptoprest  12303  cnmpt2t  12357  psmetsym  12393  psmetge0  12395  xmetge0  12429  xmetsym  12432  blvalps  12452  blval  12453  ssblps  12489  ssbl  12490  blpnfctr  12503  xmssym  12533  bdxmet  12565  metcnp3  12575  dvfvalap  12702  dvid  12714  dvcnp2cntop  12715
  Copyright terms: Public domain W3C validator