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  6431  nnanq0  6440  prltlu  6469  distrprg  6563  ltexprlemm  6573  recexprlem1ssl  6604  recexprlem1ssu  6605  addsrpr  6653  mulsrpr  6654  mulasssrg  6666  recexgt0sr  6681  axmulass  6737  axpre-ltadd  6750  ltxrlt  6862  subadd2  6992  addsubass  6998  nppcan  7009  nppcan3  7011  subcan2  7012  subsub2  7015  subsub4  7020  pnpcan  7026  pnncan  7028  subcan  7042  subdi  7158  ltadd1  7199  leadd1  7200  leadd2  7201  ltsubadd  7202  ltsubadd2  7203  lesubadd  7204  lesubadd2  7205  ltaddsub  7206  leaddsub  7208  lesub1  7226  lesub2  7227  ltsub1  7228  ltsub2  7229  ltaddsublt  7335  gt0add  7337  reapadd1  7360  remulext1  7363  remulext2  7364  apadd2  7373  mulext2  7377  mulap0r  7379  divap0b  7424  divcanap5  7452  dmdcanap  7460  redivclap  7469  div2negap  7473  lt2msq1  7612  ltdiv2  7614  nndivtr  7716  gtndiv  8091  eluzsub  8258  nn01to3  8308  qdivcl  8332  irrmul  8336  rpgecl  8366  ubioog  8533  ubioc1  8548  lbico1  8549  iccleub  8550  lbicc2  8602  ubicc2  8603  icoshftf1o  8609  fzen  8657  elfz1b  8702  uznfz  8715  elfzo0  8788  elfzo0z  8790  ubmelfzo  8806  fzonn0p1p1  8819  ubmelm1fzo  8832  frec2uzf1od  8853  expnegap0  8897  expgt1  8927  exprecap  8930  expaddzaplem  8932  expaddzap  8933  expmulzap  8935  expnbnd  9005  redivap  9082  imdivap  9089  cjdivap  9117
  Copyright terms: Public domain W3C validator