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

Theorem simp-4r 514
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 506 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
21adantr 272 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  516  fimax2gtri  6761  finexdc  6762  difinfsn  6951  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  suplocexprlemru  7491  suplocsrlemb  7578  suplocsrlem  7580  supinfneg  9342  infsupneg  9343  xaddf  9578  xaddval  9579  hashunlem  10501  xrmaxiflemcl  10965  xrmaxiflemlub  10968  xrmaxltsup  10978  sumeq2  11079  fsumconst  11174  cncnp  12305  neitx  12343  dedekindeulemlu  12674  suplociccreex  12677  dedekindicclemlu  12683  cnplimclemr  12713  limccnp2cntop  12721
  Copyright terms: Public domain W3C validator