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

Theorem simp-4r 542
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 534 . 2  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
21adantr 276 1  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  simp-5r  544  fimax2gtri  6915  finexdc  6916  dcfi  6994  difinfsn  7113  nnnninfeq2  7141  nninfisol  7145  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  suplocexprlemru  7732  suplocsrlemb  7819  suplocsrlem  7821  aptap  8621  supinfneg  9609  infsupneg  9610  xaddf  9858  xaddval  9859  nn0ltexp2  10703  hashunlem  10798  xrmaxiflemcl  11267  xrmaxiflemlub  11270  xrmaxltsup  11280  sumeq2  11381  fsumconst  11476  prodeq2  11579  fprodconst  11642  sgrpidmndm  12843  mhmmnd  13011  ghmcmn  13163  issrg  13217  cncnp  14026  neitx  14064  dedekindeulemlu  14395  suplociccreex  14398  dedekindicclemlu  14404  cnplimclemr  14434  limccnp2cntop  14442  logbgcd1irrap  14684  lgsval  14701
  Copyright terms: Public domain W3C validator