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

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

Proof of Theorem simp3
StepHypRef Expression
1 3simpc 938 . 2 ((𝜑𝜓𝜒) → (𝜓𝜒))
21simprd 112 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  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  simpl3  944  simpr3  947  simp3i  950  simp3d  953  simp13  971  simp23  974  simp33  977  3anibar  1107  3ianorr  1241  stoic4a  1362  stoic4b  1363  mob2  2773  sotri2  4752  sotri3  4753  feq123  5069  resasplitss  5100  sefvex  5227  ftpg  5379  fsnunf  5394  fnfvima  5425  cocan1  5458  cocan2  5459  f1oiso2  5497  riotass  5526  moriotass  5527  ovmpt2x  5660  ovmpt2ga  5661  caovimo  5725  ofrval  5753  dfsmo2  5936  tfr1onlembfn  5993  tfrcllembfn  6006  freccllem  6051  frecfcllem  6053  frecsuclem  6055  frecrdg  6057  nnsucsssuc  6136  f1oen2g  6302  f1dom2g  6303  xpdom3m  6378  diffifi  6428  unfidisj  6442  undiffi  6443  mulcanenq  6637  ltanqg  6652  addnnnq0  6701  nnanq0  6710  prltlu  6739  distrprg  6840  ltexprlemm  6852  recexprlem1ssl  6885  recexprlem1ssu  6886  addsrpr  6984  mulsrpr  6985  mulasssrg  6997  recexgt0sr  7012  axmulass  7101  axpre-ltadd  7114  ltxrlt  7245  subadd2  7379  addsubass  7385  nppcan  7397  nppcan3  7399  subcan2  7400  subsub2  7403  subsub4  7408  pnpcan  7414  pnncan  7416  subcan  7430  subdi  7556  ltadd1  7600  leadd1  7601  leadd2  7602  ltsubadd  7603  ltsubadd2  7604  lesubadd  7605  lesubadd2  7606  ltaddsub  7607  leaddsub  7609  lesub1  7627  lesub2  7628  ltsub1  7629  ltsub2  7630  ltaddsublt  7738  gt0add  7740  reapadd1  7763  remulext1  7766  remulext2  7767  apadd2  7776  mulext2  7780  mulap0r  7782  leltap  7791  ltap  7798  divap0b  7838  divmulasscomap  7851  divcanap5  7869  dmdcanap  7877  redivclap  7886  div2negap  7890  lt2msq1  8030  ltdiv2  8032  nndivtr  8147  gtndiv  8523  eluzsub  8729  nn01to3  8783  qdivcl  8809  irrmul  8813  rpgecl  8843  divge1  8881  ubioog  9013  ubioc1  9028  lbico1  9029  iccleub  9030  lbicc2  9082  ubicc2  9083  icoshftf1o  9089  fzen  9138  elfz1b  9183  uznfz  9196  elfzo0  9268  elfzo0z  9270  ubmelfzo  9286  fzonn0p1p1  9299  ubmelm1fzo  9312  qbtwnre  9343  flqwordi  9370  flltdivnn0lt  9386  ceiqle  9395  modqval  9406  modqvalr  9407  modqcl  9408  flqpmodeq  9409  modq0  9411  mulqmod0  9412  negqmod0  9413  modqge0  9414  modqlt  9415  modqdiffl  9417  modqdifz  9418  modqmulnn  9424  modqvalp1  9425  modqabs2  9440  modqmuladdnn0  9450  qnegmod  9451  addmodid  9454  modqeqmodmin  9476  modfzo0difsn  9477  addmodlteq  9480  frec2uzf1od  9488  expnegap0  9581  expgt1  9611  exprecap  9614  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  mulbinom2  9686  expnbnd  9693  shftfibg  9846  redivap  9899  imdivap  9906  cjdivap  9934  maxleast  10237  lemininf  10253  ltmininf  10254  climuni  10270  summodnegmod  10371  dvdsmultr2  10380  mulmoddvds  10408  divalglemeuneg  10467  gcdaddm  10519  gcdass  10548  mulgcd  10549  gcddiv  10552  lcmass  10611  mulgcddvds  10620  qredeq  10622  congr  10626  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  prmexpb  10674  rpexp  10676  unennn  10708
  Copyright terms: Public domain W3C validator