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

Theorem simp3 905
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp3 ((φ ψ χ) → χ)

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 902 . 2 ((φ ψ χ) → (ψ χ))
21simprd 107 1 ((φ ψ χ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simpl3  908  simpr3  911  simp3i  914  simp3d  917  simp13  935  simp23  938  simp33  941  3anibar  1071  3ianorr  1203  stoic4a  1318  stoic4b  1319  mob2  2715  sotri2  4665  sotri3  4666  feq123  4981  resasplitss  5012  sefvex  5139  ftpg  5290  fsnunf  5305  fnfvima  5336  cocan1  5370  cocan2  5371  f1oiso2  5409  riotass  5438  moriotass  5439  ovmpt2x  5571  ovmpt2ga  5572  caovimo  5636  ofrval  5664  dfsmo2  5843  nnsucsssuc  6010  f1oen2g  6171  f1dom2g  6172  xpdom3m  6244  mulcanenq  6369  ltanqg  6384  addnnnq0  6432  nnanq0  6441  prltlu  6470  distrprg  6564  ltexprlemm  6574  recexprlem1ssl  6605  recexprlem1ssu  6606  addsrpr  6673  mulsrpr  6674  mulasssrg  6686  recexgt0sr  6701  axmulass  6757  axpre-ltadd  6770  ltxrlt  6882  subadd2  7012  addsubass  7018  nppcan  7029  nppcan3  7031  subcan2  7032  subsub2  7035  subsub4  7040  pnpcan  7046  pnncan  7048  subcan  7062  subdi  7178  ltadd1  7219  leadd1  7220  leadd2  7221  ltsubadd  7222  ltsubadd2  7223  lesubadd  7224  lesubadd2  7225  ltaddsub  7226  leaddsub  7228  lesub1  7246  lesub2  7247  ltsub1  7248  ltsub2  7249  ltaddsublt  7355  gt0add  7357  reapadd1  7380  remulext1  7383  remulext2  7384  apadd2  7393  mulext2  7397  mulap0r  7399  divap0b  7444  divcanap5  7472  dmdcanap  7480  redivclap  7489  div2negap  7493  lt2msq1  7632  ltdiv2  7634  nndivtr  7736  gtndiv  8111  eluzsub  8278  nn01to3  8328  qdivcl  8352  irrmul  8356  rpgecl  8386  ubioog  8553  ubioc1  8568  lbico1  8569  iccleub  8570  lbicc2  8622  ubicc2  8623  icoshftf1o  8629  fzen  8677  elfz1b  8722  uznfz  8735  elfzo0  8808  elfzo0z  8810  ubmelfzo  8826  fzonn0p1p1  8839  ubmelm1fzo  8852  frec2uzf1od  8873  expnegap0  8917  expgt1  8947  exprecap  8950  expaddzaplem  8952  expaddzap  8953  expmulzap  8955  expnbnd  9025  redivap  9102  imdivap  9109  cjdivap  9137
  Copyright terms: Public domain W3C validator