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

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

Proof of Theorem simp2
StepHypRef Expression
1 3simpa 901 . 2 ((𝜑𝜓𝜒) → (𝜑𝜓))
21simprd 107 1 ((𝜑𝜓𝜒) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  simpl2  908  simpr2  911  simp2i  914  simp2d  917  simp12  935  simp22  938  simp32  941  syld3an3  1180  3ianorr  1204  stoic4b  1322  nlim0  4131  tfisi  4310  sotri2  4722  sotri3  4723  feq123  5038  sefvex  5196  fvmptt  5262  fnfvima  5393  cocan1  5427  cocan2  5428  ovexg  5539  ovmpt2x  5629  ovmpt2ga  5630  caovimo  5694  frecsuclem3  5990  dif1en  6337  diffifi  6351  mulcanenq  6481  ltanqg  6496  mulcanenq0ec  6541  addnnnq0  6545  distrprg  6684  aptipr  6737  addsrpr  6828  mulsrpr  6829  mulasssrg  6841  axmulass  6945  axpre-ltadd  6958  subadd2  7213  nppcan  7231  nppcan3  7233  subsub2  7237  subsub4  7242  npncan3  7247  pnpcan  7248  pnncan  7250  subcan  7264  ltadd1  7422  leadd1  7423  leadd2  7424  ltsubadd  7425  ltsubadd2  7426  lesubadd  7427  lesubadd2  7428  ltaddsub  7429  leaddsub  7431  lesub1  7449  lesub2  7450  ltsub1  7451  ltsub2  7452  gt0add  7562  apreap  7576  lemul1  7582  reapmul1lem  7583  reapmul1  7584  reapadd1  7585  remulext1  7588  remulext2  7589  apadd2  7598  mulext2  7602  mulap0r  7604  leltap  7613  ltap  7620  recexaplem2  7631  mulcanap  7644  mulcanap2  7645  divvalap  7651  divmulap  7652  divcanap1  7658  diveqap0  7659  divap0b  7660  divrecap  7665  divassap  7667  div23ap  7668  divdirap  7672  divcanap3  7673  div11ap  7675  diveqap1  7680  divmuldivap  7686  divcanap5  7688  redivclap  7705  div2negap  7709  apmul1  7762  ltdiv1  7832  ledivmul  7841  lemuldiv  7845  lt2msq1  7849  ltdiv23  7856  squeeze0  7868  zaddcllemneg  8282  eluzsub  8500  nn01to3  8550  rpgecl  8609  lbioog  8780  ubioc1  8796  ubicc2  8851  icoshftf1o  8857  fzen  8905  ubmelfzo  9054  ssfzo12  9078  ubmelm1fzo  9080  fzosplitprm1  9088  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  qbtwnre  9109  flqwordi  9128  flqword2  9129  flltdivnn0lt  9144  frec2uzf1od  9166  expnegap0  9237  expgt1  9267  exprecap  9270  expmulzap  9275  leexp2a  9281  expubnd  9285  bernneq2  9344  expnbnd  9346  shftuz  9392  shftfibg  9395  cjdivap  9483  resqrtcl  9601  absdivap  9642  abssubne0  9661  climuni  9787  findset  10043
  Copyright terms: Public domain W3C validator