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

Theorem simp3 968
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 965 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
21simprd 113 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 947
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 949
This theorem is referenced by:  simpl3  971  simpr3  974  simp3i  977  simp3d  980  simp13  998  simp23  1001  simp33  1004  3anibar  1134  3ianorr  1272  stoic4a  1393  stoic4b  1394  mob2  2837  sotri2  4906  sotri3  4907  feq123  5234  resasplitss  5272  sefvex  5410  ftpg  5572  fsnunf  5588  fnfvima  5620  cocan1  5656  cocan2  5657  f1oiso2  5696  riotass  5725  moriotass  5726  ovmpox  5867  ovmpoga  5868  caovimo  5932  ofrval  5960  dfsmo2  6152  tfr1onlembfn  6209  tfrcllembfn  6222  freccllem  6267  frecfcllem  6269  frecsuclem  6271  frecrdg  6273  nnsucsssuc  6356  f1oen2g  6617  f1dom2g  6618  xpdom3m  6696  mapxpen  6710  diffifi  6756  unfidisj  6778  undifdc  6780  ssfidc  6791  sbthlemi9  6821  ctssdc  6966  endjudisj  7034  djuassen  7041  xpdjuen  7042  mulcanenq  7161  ltanqg  7176  addnnnq0  7225  nnanq0  7234  prltlu  7263  distrprg  7364  ltexprlemm  7376  recexprlem1ssl  7409  recexprlem1ssu  7410  addsrpr  7521  mulsrpr  7522  mulasssrg  7534  recexgt0sr  7549  ltpsrprg  7579  axmulass  7649  axpre-ltadd  7662  ltxrlt  7798  subadd2  7934  addsubass  7940  nppcan  7952  nppcan3  7954  subcan2  7955  subsub2  7958  subsub4  7963  pnpcan  7969  pnncan  7971  subcan  7985  subdi  8115  ltadd1  8159  leadd1  8160  leadd2  8161  ltsubadd  8162  ltsubadd2  8163  lesubadd  8164  lesubadd2  8165  ltaddsub  8166  leaddsub  8168  lesub1  8186  lesub2  8187  ltsub1  8188  ltsub2  8189  ltaddsublt  8301  gt0add  8303  reapadd1  8326  remulext1  8329  remulext2  8330  apadd2  8339  mulext2  8343  mulap0r  8345  leltap  8355  ltap  8363  apsub1  8372  divap0b  8411  divmulasscomap  8424  divcanap5  8442  dmdcanap  8450  redivclap  8459  div2negap  8463  lt2msq1  8611  ltdiv2  8613  nndivtr  8730  gtndiv  9114  eluzsub  9323  nn01to3  9377  qdivcl  9403  irrmul  9407  rpgecl  9438  divge1  9478  xaddass  9620  xltadd1  9627  ubioog  9665  ubioc1  9680  lbico1  9681  iccleub  9682  lbicc2  9735  ubicc2  9736  icoshftf1o  9742  fzen  9791  elfz1b  9838  uznfz  9851  elfzo0  9927  elfzo0z  9929  ubmelfzo  9945  fzonn0p1p1  9958  ubmelm1fzo  9971  qbtwnre  10002  flqwordi  10029  flltdivnn0lt  10045  ceiqle  10054  modqval  10065  modqvalr  10066  modqcl  10067  flqpmodeq  10068  modq0  10070  mulqmod0  10071  negqmod0  10072  modqge0  10073  modqlt  10074  modqdiffl  10076  modqdifz  10077  modqmulnn  10083  modqvalp1  10084  modqabs2  10099  modqmuladdnn0  10109  qnegmod  10110  addmodid  10113  modqeqmodmin  10135  modfzo0difsn  10136  addmodlteq  10139  frec2uzf1od  10147  expnegap0  10269  expgt1  10299  exprecap  10302  expaddzaplem  10304  expaddzap  10305  expmulzap  10307  mulbinom2  10376  expnbnd  10383  fihashss  10530  fimaxq  10541  seq3coll  10553  shftfibg  10560  redivap  10614  imdivap  10621  cjdivap  10649  maxleast  10953  lemininf  10973  ltmininf  10974  bdtrilem  10978  bdtri  10979  xrmaxaddlem  10997  xrmaxadd  10998  xrmineqinf  11006  xrltmininf  11007  xrminltinf  11009  xrminadd  11012  climuni  11030  reccn2ap  11050  isumz  11126  fsumsplitsnun  11156  geoisum1c  11257  cos12dec  11401  summodnegmod  11451  dvdsmultr2  11460  mulmoddvds  11488  divalglemeuneg  11547  gcdaddm  11599  gcdass  11630  mulgcd  11631  gcddiv  11634  lcmass  11693  mulgcddvds  11702  qredeq  11704  congr  11708  divgcdcoprmex  11710  cncongr1  11711  cncongr2  11712  prmexpb  11756  rpexp  11758  unennn  11837  fvsetsid  11920  ressid2  11945  ressval2  11946  rngmulrg  12004  basgen  12176  2basgeng  12178  ntrss  12215  neiss  12246  opnneiss  12254  restco  12270  restabs  12271  cnprcl2k  12302  cnpf2  12303  lmconst  12312  cnpnei  12315  cnptoprest  12335  cnmpt2t  12389  psmetsym  12425  psmetge0  12427  xmetge0  12461  xmetsym  12464  blvalps  12484  blval  12485  ssblps  12521  ssbl  12522  blpnfctr  12535  xmssym  12565  bdxmet  12597  metcnp3  12607  dvfvalap  12746  dvid  12758  dvcnp2cntop  12759  ptolemy  12832
  Copyright terms: Public domain W3C validator