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

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

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 940 . 2 ((𝜑𝜓𝜒) → (𝜓𝜒))
21simprd 112 1 ((𝜑𝜓𝜒) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  simpl3  946  simpr3  949  simp3i  952  simp3d  955  simp13  973  simp23  976  simp33  979  3anibar  1109  3ianorr  1243  stoic4a  1364  stoic4b  1365  mob2  2786  sotri2  4796  sotri3  4797  feq123  5118  resasplitss  5153  sefvex  5289  ftpg  5444  fsnunf  5459  fnfvima  5490  cocan1  5527  cocan2  5528  f1oiso2  5567  riotass  5596  moriotass  5597  ovmpt2x  5730  ovmpt2ga  5731  caovimo  5795  ofrval  5823  dfsmo2  6006  tfr1onlembfn  6063  tfrcllembfn  6076  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecrdg  6127  nnsucsssuc  6207  f1oen2g  6424  f1dom2g  6425  xpdom3m  6502  mapxpen  6516  diffifi  6562  unfidisj  6584  undifdc  6586  ssfidc  6594  sbthlemi9  6618  mulcanenq  6888  ltanqg  6903  addnnnq0  6952  nnanq0  6961  prltlu  6990  distrprg  7091  ltexprlemm  7103  recexprlem1ssl  7136  recexprlem1ssu  7137  addsrpr  7235  mulsrpr  7236  mulasssrg  7248  recexgt0sr  7263  axmulass  7352  axpre-ltadd  7365  ltxrlt  7496  subadd2  7630  addsubass  7636  nppcan  7648  nppcan3  7650  subcan2  7651  subsub2  7654  subsub4  7659  pnpcan  7665  pnncan  7667  subcan  7681  subdi  7807  ltadd1  7851  leadd1  7852  leadd2  7853  ltsubadd  7854  ltsubadd2  7855  lesubadd  7856  lesubadd2  7857  ltaddsub  7858  leaddsub  7860  lesub1  7878  lesub2  7879  ltsub1  7880  ltsub2  7881  ltaddsublt  7989  gt0add  7991  reapadd1  8014  remulext1  8017  remulext2  8018  apadd2  8027  mulext2  8031  mulap0r  8033  leltap  8042  ltap  8049  divap0b  8089  divmulasscomap  8102  divcanap5  8120  dmdcanap  8128  redivclap  8137  div2negap  8141  lt2msq1  8281  ltdiv2  8283  nndivtr  8398  gtndiv  8774  eluzsub  8980  nn01to3  9034  qdivcl  9060  irrmul  9064  rpgecl  9094  divge1  9132  ubioog  9264  ubioc1  9279  lbico1  9280  iccleub  9281  lbicc2  9333  ubicc2  9334  icoshftf1o  9340  fzen  9389  elfz1b  9434  uznfz  9447  elfzo0  9521  elfzo0z  9523  ubmelfzo  9539  fzonn0p1p1  9552  ubmelm1fzo  9565  qbtwnre  9596  flqwordi  9623  flltdivnn0lt  9639  ceiqle  9648  modqval  9659  modqvalr  9660  modqcl  9661  flqpmodeq  9662  modq0  9664  mulqmod0  9665  negqmod0  9666  modqge0  9667  modqlt  9668  modqdiffl  9670  modqdifz  9671  modqmulnn  9677  modqvalp1  9678  modqabs2  9693  modqmuladdnn0  9703  qnegmod  9704  addmodid  9707  modqeqmodmin  9729  modfzo0difsn  9730  addmodlteq  9733  frec2uzf1od  9741  expnegap0  9861  expgt1  9891  exprecap  9894  expaddzaplem  9896  expaddzap  9897  expmulzap  9899  mulbinom2  9966  expnbnd  9973  fihashss  10120  fimaxq  10131  iseqcoll  10143  shftfibg  10150  redivap  10203  imdivap  10210  cjdivap  10238  maxleast  10541  lemininf  10557  ltmininf  10558  climuni  10574  isumz  10667  summodnegmod  10702  dvdsmultr2  10711  mulmoddvds  10739  divalglemeuneg  10798  gcdaddm  10850  gcdass  10879  mulgcd  10880  gcddiv  10883  lcmass  10942  mulgcddvds  10951  qredeq  10953  congr  10957  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  prmexpb  11005  rpexp  11007  unennn  11085
  Copyright terms: Public domain W3C validator