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

Theorem simpllr 494
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simpllr  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 107 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 465 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  f1o2ndf1  5876  tfrlem1  5953  fopwdom  6340  phplem4dom  6354  phpm  6357  phplem4on  6359  fidifsnen  6361  diffisn  6380  diffifi  6381  addcmpblnq  6522  mulcmpblnq  6523  ordpipqqs  6529  ltexnqq  6563  enq0tr  6589  addcmpblnq0  6598  mulcmpblnq0  6599  nnnq0lem1  6601  prssnqu  6635  prarloclemup  6650  nqprl  6706  nqpru  6707  mullocpr  6726  cauappcvgprlemladdfu  6809  cauappcvgprlemladdrl  6812  caucvgprlemm  6823  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlemlim  6836  caucvgprprlemml  6849  caucvgprprlemloc  6858  caucvgprprlemlim  6866  addcmpblnr  6881  mulcmpblnrlemg  6882  mulcmpblnr  6883  ltsrprg  6889  srpospr  6924  caucvgsrlemoffres  6941  axcaucvglemcau  7029  cnegexlem3  7250  negeu  7264  add20  7542  rimul  7649  apreap  7651  cru  7666  apreim  7667  apsym  7670  apcotr  7671  apadd1  7672  apneg  7675  mulext1  7676  apti  7686  mulap0  7708  prodgt0  7892  ltmul12a  7900  ledivdiv  7930  lediv12a  7934  qapne  8670  ixxss12  8875  ioodisj  8961  fznlem  9006  qtri3or  9199  qbtwnzlemstep  9204  rebtwn2zlemstep  9208  addmodlteq  9347  mulexpzap  9459  leexp1a  9474  expnbnd  9539  faclbnd  9608  cjap  9733  caucvgre  9807  cvg1nlemres  9811  resqrexlemglsq  9848  resqrexlemga  9849  sqrtsq  9870  ltabs  9913  abs3lem  9937  cau3lem  9940  climcau  10096  climrecvg1n  10097  dvdsle  10155  pw2dvdslemn  10232  oddpwdclemxy  10236
  Copyright terms: Public domain W3C validator