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

Theorem simp1 939
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp1 ((𝜑𝜓𝜒) → 𝜑)

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 936 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simpld 110 1 ((𝜑𝜓𝜒) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpl1  942  simpr1  945  simp1i  948  simp1d  951  simp11  969  simp21  972  simp31  975  syld3an3  1215  3ianorr  1241  stoic4a  1362  stoic4b  1363  rsp2e  2415  issod  4082  elirr  4292  sotri2  4752  sotri3  4753  funtpg  4981  funimaexglem  5013  feq123  5069  foco2  5350  ftpg  5379  fsnunf  5394  fcofo  5455  f1oiso2  5497  riotass  5526  ovmpt2x  5660  ovmpt2ga  5661  caovimo  5725  ofeq  5745  ofrval  5753  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  frecsuclem  6055  frecrdg  6057  diffifi  6428  unsnfidcex  6440  unsnfidcel  6441  unfidisj  6442  undiffi  6443  mulcanenq  6637  ltanqg  6652  addnnnq0  6701  distrlem4prl  6836  distrlem4pru  6837  distrprg  6840  aptipr  6893  addsrpr  6984  mulsrpr  6985  mulasssrg  6997  axmulass  7101  axpre-ltadd  7114  mul31  7306  addsubass  7385  subcan2  7400  subsub2  7403  subsub4  7408  npncan3  7413  pnpcan  7414  pnncan  7416  subcan  7430  subdi  7556  ltadd1  7600  leadd1  7601  leadd2  7602  ltsubadd  7603  lesubadd  7605  ltaddsub  7607  leaddsub  7609  lesub1  7627  lesub2  7628  ltsub1  7629  ltsub2  7630  ltaddsublt  7738  gt0add  7740  apreap  7754  lemul1  7760  reapmul1lem  7761  reapmul1  7762  reapadd1  7763  remulext1  7766  remulext2  7767  apadd2  7776  mulext2  7780  mulap0r  7782  leltap  7791  ltap  7798  recexaplem2  7809  mulcanap  7822  mulcanap2  7823  divvalap  7829  divcanap2  7835  diveqap0  7837  divrecap  7843  divrecap2  7844  divdirap  7852  divcanap3  7853  div11ap  7855  muldivdirap  7862  divcanap5  7869  redivclap  7886  div2negap  7890  apmul1  7943  ltdiv1  8013  ltmuldiv  8019  lemuldiv  8026  lt2msq1  8030  ltdiv23  8037  lediv23  8038  squeeze0  8049  gtndiv  8523  eluz2  8706  eluzsub  8729  peano2uz  8752  nn01to3  8783  divge1  8881  ledivge1le  8884  addlelt  8920  ixxssixx  9001  lbico1  9029  lbicc2  9082  icoshftf1o  9089  fzen  9138  fzrev3  9180  fzrevral2  9199  elfzo0  9268  elfzo0z  9270  fzosplitprm1  9320  qbtwnre  9343  flqwordi  9370  flqword2  9371  adddivflid  9374  flltdivnn0lt  9386  modqcl  9408  mulqmod0  9412  modqmulnn  9424  modqabs2  9440  addmodid  9454  modifeq2int  9468  modqeqmodmin  9476  iseqeq2  9525  iseqeq3  9526  expnegap0  9581  expgt1  9611  exprecap  9614  leexp2a  9626  expubnd  9630  sqdivap  9637  expnbnd  9693  bccmpl  9778  shftfibg  9846  mulreap  9889  abssubne0  10115  maxleast  10237  lemininf  10253  ltmininf  10254  climuni  10270  dvdscmulr  10369  dvdsmulcr  10370  summodnegmod  10371  modmulconst  10372  dvdsmultr2  10380  dvdsexp  10406  mulmoddvds  10408  modremain  10473  divgcdz  10507  gcdaddm  10519  dvdsgcdb  10546  gcdass  10548  mulgcd  10549  gcddiv  10552  rplpwr  10560  lcmdvdsb  10610  lcmass  10611  mulgcddvds  10620  qredeq  10622  qredeu  10623  rpmul  10624  divgcdcoprmex  10628  cncongr1  10629  rpexp  10676  rpexp12i  10678
  Copyright terms: Public domain W3C validator