ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simp-4r Unicode version

Theorem simp-4r 516
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-4r  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )

Proof of Theorem simp-4r
StepHypRef Expression
1 simpllr 508 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
21adantr 274 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  simp-5r  518  fimax2gtri  6763  finexdc  6764  difinfsn  6953  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  suplocexprlemru  7495  suplocsrlemb  7582  suplocsrlem  7584  supinfneg  9358  infsupneg  9359  xaddf  9595  xaddval  9596  hashunlem  10518  xrmaxiflemcl  10982  xrmaxiflemlub  10985  xrmaxltsup  10995  sumeq2  11096  fsumconst  11191  cncnp  12326  neitx  12364  dedekindeulemlu  12695  suplociccreex  12698  dedekindicclemlu  12704  cnplimclemr  12734  limccnp2cntop  12742
  Copyright terms: Public domain W3C validator