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

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

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 900 . 2 ((φ ψ χ) → (φ ψ))
21simpld 105 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
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  simpl1  906  simpr1  909  simp1i  912  simp1d  915  simp11  933  simp21  936  simp31  939  syld3an3  1179  3ianorr  1203  stoic4a  1318  stoic4b  1319  rsp2e  2366  issod  4047  elirr  4224  sotri2  4665  sotri3  4666  funtpg  4893  funimaexglem  4925  feq123  4981  foco2  5261  ftpg  5290  fsnunf  5305  fcofo  5367  f1oiso2  5409  riotass  5438  ovmpt2x  5571  ovmpt2ga  5572  caovimo  5636  ofeq  5656  ofrval  5664  frecsuclem3  5929  mulcanenq  6369  ltanqg  6384  addnnnq0  6432  distrlem4prl  6560  distrlem4pru  6561  distrprg  6564  aptipr  6613  addsrpr  6673  mulsrpr  6674  mulasssrg  6686  axmulass  6757  axpre-ltadd  6770  mul31  6941  addsubass  7018  subcan2  7032  subsub2  7035  subsub4  7040  npncan3  7045  pnpcan  7046  pnncan  7048  subcan  7062  subdi  7178  ltadd1  7219  leadd1  7220  leadd2  7221  ltsubadd  7222  lesubadd  7224  ltaddsub  7226  leaddsub  7228  lesub1  7246  lesub2  7247  ltsub1  7248  ltsub2  7249  ltaddsublt  7355  gt0add  7357  apreap  7371  lemul1  7377  reapmul1lem  7378  reapmul1  7379  reapadd1  7380  remulext1  7383  remulext2  7384  apadd2  7393  mulext2  7397  mulap0r  7399  recexaplem2  7415  mulcanap  7428  mulcanap2  7429  divvalap  7435  divcanap2  7441  diveqap0  7443  divrecap  7449  divrecap2  7450  divdirap  7456  divcanap3  7457  div11ap  7459  divcanap5  7472  redivclap  7489  div2negap  7493  apmul1  7546  ltdiv1  7615  ltmuldiv  7621  lemuldiv  7628  lt2msq1  7632  ltdiv23  7639  lediv23  7640  squeeze0  7651  gtndiv  8111  eluz2  8255  eluzsub  8278  peano2uz  8302  nn01to3  8328  ixxssixx  8541  lbico1  8569  lbicc2  8622  icoshftf1o  8629  fzen  8677  fzrev3  8719  fzrevral2  8738  elfzo0  8808  elfzo0z  8810  fzosplitprm1  8860  iseqeq2  8895  iseqeq3  8896  expnegap0  8917  expgt1  8947  exprecap  8950  leexp2a  8961  expubnd  8965  sqdivap  8972  expnbnd  9025  mulreap  9092
  Copyright terms: Public domain W3C validator