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

Theorem simp3 917
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 914 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ps  /\  ch ) )
21simprd 111 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl3  920  simpr3  923  simp3i  926  simp3d  929  simp13  947  simp23  950  simp33  953  3anibar  1083  3ianorr  1215  stoic4a  1337  stoic4b  1338  mob2  2744  sotri2  4750  sotri3  4751  feq123  5066  resasplitss  5097  sefvex  5224  ftpg  5375  fsnunf  5390  fnfvima  5421  cocan1  5455  cocan2  5456  f1oiso2  5494  riotass  5523  moriotass  5524  ovmpt2x  5657  ovmpt2ga  5658  caovimo  5722  ofrval  5750  dfsmo2  5933  nnsucsssuc  6102  f1oen2g  6266  f1dom2g  6267  xpdom3m  6339  diffifi  6382  mulcanenq  6541  ltanqg  6556  addnnnq0  6605  nnanq0  6614  prltlu  6643  distrprg  6744  ltexprlemm  6756  recexprlem1ssl  6789  recexprlem1ssu  6790  addsrpr  6888  mulsrpr  6889  mulasssrg  6901  recexgt0sr  6916  axmulass  7005  axpre-ltadd  7018  ltxrlt  7144  subadd2  7278  addsubass  7284  nppcan  7296  nppcan3  7298  subcan2  7299  subsub2  7302  subsub4  7307  pnpcan  7313  pnncan  7315  subcan  7329  subdi  7454  ltadd1  7498  leadd1  7499  leadd2  7500  ltsubadd  7501  ltsubadd2  7502  lesubadd  7503  lesubadd2  7504  ltaddsub  7505  leaddsub  7507  lesub1  7525  lesub2  7526  ltsub1  7527  ltsub2  7528  ltaddsublt  7636  gt0add  7638  reapadd1  7661  remulext1  7664  remulext2  7665  apadd2  7674  mulext2  7678  mulap0r  7680  leltap  7689  ltap  7696  divap0b  7736  divcanap5  7765  dmdcanap  7773  redivclap  7782  div2negap  7786  lt2msq1  7926  ltdiv2  7928  nndivtr  8031  gtndiv  8393  eluzsub  8598  nn01to3  8649  qdivcl  8675  irrmul  8679  rpgecl  8709  divge1  8747  ubioog  8884  ubioc1  8899  lbico1  8900  iccleub  8901  lbicc2  8953  ubicc2  8954  icoshftf1o  8960  fzen  9009  elfz1b  9054  uznfz  9067  elfzo0  9140  elfzo0z  9142  ubmelfzo  9158  fzonn0p1p1  9171  ubmelm1fzo  9184  qbtwnre  9213  flqwordi  9238  flltdivnn0lt  9254  ceiqle  9263  modqval  9274  modqvalr  9275  modqcl  9276  flqpmodeq  9277  modq0  9279  mulqmod0  9280  negqmod0  9281  modqge0  9282  modqlt  9283  modqdiffl  9285  modqdifz  9286  modqmulnn  9292  modqvalp1  9293  modqabs2  9308  modqmuladdnn0  9318  qnegmod  9319  addmodid  9322  modqeqmodmin  9344  modfzo0difsn  9345  addmodlteq  9348  frec2uzf1od  9356  expnegap0  9428  expgt1  9458  exprecap  9461  expaddzaplem  9463  expaddzap  9464  expmulzap  9466  mulbinom2  9533  expnbnd  9540  shftfibg  9649  redivap  9702  imdivap  9709  cjdivap  9737  climuni  10045  summodnegmod  10138  dvdsmultr2  10147  mulmoddvds  10175  divalglemeuneg  10235
  Copyright terms: Public domain W3C validator