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

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

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 914 . 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  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  simpl3  920  simpr3  923  simp3i  926  simp3d  929  simp13  947  simp23  950  simp33  953  3anibar  1083  3ianorr  1215  stoic4a  1337  stoic4b  1338  mob2  2743  sotri2  4749  sotri3  4750  feq123  5065  resasplitss  5096  sefvex  5223  ftpg  5374  fsnunf  5389  fnfvima  5420  cocan1  5454  cocan2  5455  f1oiso2  5493  riotass  5522  moriotass  5523  ovmpt2x  5656  ovmpt2ga  5657  caovimo  5721  ofrval  5749  dfsmo2  5932  nnsucsssuc  6101  f1oen2g  6265  f1dom2g  6266  xpdom3m  6338  diffifi  6381  mulcanenq  6540  ltanqg  6555  addnnnq0  6604  nnanq0  6613  prltlu  6642  distrprg  6743  ltexprlemm  6755  recexprlem1ssl  6788  recexprlem1ssu  6789  addsrpr  6887  mulsrpr  6888  mulasssrg  6900  recexgt0sr  6915  axmulass  7004  axpre-ltadd  7017  ltxrlt  7143  subadd2  7277  addsubass  7283  nppcan  7295  nppcan3  7297  subcan2  7298  subsub2  7301  subsub4  7306  pnpcan  7312  pnncan  7314  subcan  7328  subdi  7453  ltadd1  7497  leadd1  7498  leadd2  7499  ltsubadd  7500  ltsubadd2  7501  lesubadd  7502  lesubadd2  7503  ltaddsub  7504  leaddsub  7506  lesub1  7524  lesub2  7525  ltsub1  7526  ltsub2  7527  ltaddsublt  7635  gt0add  7637  reapadd1  7660  remulext1  7663  remulext2  7664  apadd2  7673  mulext2  7677  mulap0r  7679  leltap  7688  ltap  7695  divap0b  7735  divcanap5  7764  dmdcanap  7772  redivclap  7781  div2negap  7785  lt2msq1  7925  ltdiv2  7927  nndivtr  8030  gtndiv  8392  eluzsub  8597  nn01to3  8648  qdivcl  8674  irrmul  8678  rpgecl  8708  divge1  8746  ubioog  8883  ubioc1  8898  lbico1  8899  iccleub  8900  lbicc2  8952  ubicc2  8953  icoshftf1o  8959  fzen  9008  elfz1b  9053  uznfz  9066  elfzo0  9139  elfzo0z  9141  ubmelfzo  9157  fzonn0p1p1  9170  ubmelm1fzo  9183  qbtwnre  9212  flqwordi  9232  flltdivnn0lt  9248  ceiqle  9257  modqval  9268  modqvalr  9269  modqcl  9270  flqpmodeq  9271  modq0  9273  mulqmod0  9274  negqmod0  9275  modqge0  9276  modqlt  9277  modqdiffl  9279  modqdifz  9280  modqmulnn  9286  modqvalp1  9287  modqabs2  9302  modqmuladdnn0  9312  qnegmod  9313  addmodid  9316  modqeqmodmin  9338  modfzo0difsn  9339  addmodlteq  9342  frec2uzf1od  9350  expnegap0  9422  expgt1  9452  exprecap  9455  expaddzaplem  9457  expaddzap  9458  expmulzap  9460  mulbinom2  9526  expnbnd  9533  shftfibg  9642  redivap  9695  imdivap  9702  cjdivap  9730  climuni  10037  summodnegmod  10130  dvdsmultr2  10139  mulmoddvds  10167
  Copyright terms: Public domain W3C validator