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

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

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 912 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simprd 111 1 ((𝜑𝜓𝜒) → 𝜓)
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
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl2  919  simpr2  922  simp2i  925  simp2d  928  simp12  946  simp22  949  simp32  952  syld3an3  1191  3ianorr  1215  stoic4b  1338  nlim0  4159  tfisi  4338  sotri2  4750  sotri3  4751  feq123  5066  sefvex  5224  fvmptt  5290  fnfvima  5421  cocan1  5455  cocan2  5456  ovexg  5567  ovmpt2x  5657  ovmpt2ga  5658  caovimo  5722  frecsuclem3  6021  dif1en  6368  diffifi  6382  mulcanenq  6541  ltanqg  6556  mulcanenq0ec  6601  addnnnq0  6605  distrprg  6744  aptipr  6797  addsrpr  6888  mulsrpr  6889  mulasssrg  6901  axmulass  7005  axpre-ltadd  7018  subadd2  7278  nppcan  7296  nppcan3  7298  subsub2  7302  subsub4  7307  npncan3  7312  pnpcan  7313  pnncan  7315  subcan  7329  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  gt0add  7638  apreap  7652  lemul1  7658  reapmul1lem  7659  reapmul1  7660  reapadd1  7661  remulext1  7664  remulext2  7665  apadd2  7674  mulext2  7678  mulap0r  7680  leltap  7689  ltap  7696  recexaplem2  7707  mulcanap  7720  mulcanap2  7721  divvalap  7727  divmulap  7728  divcanap1  7734  diveqap0  7735  divap0b  7736  divrecap  7741  divassap  7743  div23ap  7744  divdirap  7748  divcanap3  7749  div11ap  7751  diveqap1  7756  divmuldivap  7763  divcanap5  7765  redivclap  7782  div2negap  7786  apmul1  7839  ltdiv1  7909  ledivmul  7918  lemuldiv  7922  lt2msq1  7926  ltdiv23  7933  squeeze0  7945  zaddcllemneg  8341  eluzsub  8598  nn01to3  8649  rpgecl  8709  addlelt  8786  lbioog  8883  ubioc1  8899  ubicc2  8954  icoshftf1o  8960  fzen  9009  ubmelfzo  9158  ssfzo12  9182  ubmelm1fzo  9184  fzosplitprm1  9192  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  qbtwnre  9213  flqwordi  9238  flqword2  9239  flltdivnn0lt  9254  modqcl  9276  mulqmod0  9280  modqmulnn  9292  modqabs2  9308  modqmuladdnn0  9318  qnegmod  9319  addmodid  9322  modqm1p1mod0  9325  modifeq2int  9336  modqdi  9342  modqeqmodmin  9344  modfzo0difsn  9345  frec2uzf1od  9356  expnegap0  9428  expgt1  9458  exprecap  9461  expmulzap  9466  leexp2a  9473  expubnd  9477  mulbinom2  9533  bernneq2  9538  expnbnd  9540  shftuz  9646  shftfibg  9649  cjdivap  9737  resqrtcl  9856  absdivap  9897  abssubne0  9918  climuni  10045  dvdsval2  10111  dvdscmulr  10136  dvdsmulcr  10137  modmulconst  10139  dvdsadd2b  10154  dvdsexp  10173  mulmoddvds  10175  divalglemeuneg  10235  findset  10457
  Copyright terms: Public domain W3C validator