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

Theorem simpllr 523
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 109 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 479 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  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-4r  531  f1o2ndf1  6125  tfrlem1  6205  tfr1onlemaccex  6245  tfrcllemaccex  6258  frecabcl  6296  fopwdom  6730  phplem4dom  6756  phpm  6759  phplem4on  6761  fidifsnen  6764  diffisn  6787  diffifi  6788  en2eqpr  6801  fisseneq  6820  suplub2ti  6888  difinfsn  6985  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdc  6998  enomnilem  7010  enwomnilem  7040  cc3  7090  addcmpblnq  7189  mulcmpblnq  7190  ordpipqqs  7196  ltexnqq  7230  enq0tr  7256  addcmpblnq0  7265  mulcmpblnq0  7266  nnnq0lem1  7268  prssnqu  7302  prarloclemup  7317  nqprl  7373  nqpru  7374  mullocpr  7393  cauappcvgprlemladdfu  7476  cauappcvgprlemladdrl  7479  caucvgprlemm  7490  caucvgprlemladdfu  7499  caucvgprlemladdrl  7500  caucvgprlemlim  7503  caucvgprprlemml  7516  caucvgprprlemloc  7525  caucvgprprlemlim  7533  suplocexprlemmu  7540  suplocexprlemru  7541  suplocexprlemdisj  7542  suplocexprlemloc  7543  addcmpblnr  7561  mulcmpblnrlemg  7562  mulcmpblnr  7563  ltsrprg  7569  srpospr  7605  caucvgsrlemoffres  7622  suplocsrlemb  7628  suplocsrlempr  7629  suplocsrlem  7630  axcaucvglemcau  7720  axsuploc  7851  cnegexlem3  7953  negeu  7967  add20  8250  rimul  8361  apreap  8363  cru  8378  apreim  8379  apsym  8382  apcotr  8383  apadd1  8384  apneg  8387  mulext1  8388  apti  8398  mulap0  8429  prodgt0  8624  ltmul12a  8632  ledivdiv  8662  lediv12a  8666  supinfneg  9404  infsupneg  9405  qapne  9445  xaddf  9641  xaddval  9642  xleadd1a  9670  xleaddadd  9684  ixxss12  9703  ioodisj  9790  fznlem  9835  qtri3or  10034  exbtwnzlemstep  10039  rebtwn2zlemstep  10044  addmodlteq  10185  mulexpzap  10347  leexp1a  10362  expnbnd  10429  faclbnd  10501  hashxp  10586  zfz1iso  10598  cjap  10692  caucvgre  10767  cvg1nlemres  10771  resqrexlemglsq  10808  resqrexlemga  10809  sqrtsq  10830  ltabs  10873  abs3lem  10897  cau3lem  10900  maxleim  10991  rexico  11007  minmax  11015  xrmaxleim  11027  xrmaxiflemcl  11028  xrmaxiflemlub  11031  xrmaxiflemval  11033  xrmaxltsup  11041  xrmaxadd  11044  xrminmax  11048  xrbdtri  11059  climcau  11130  climrecvg1n  11131  sumeq2  11142  summodclem2  11165  divcnv  11280  prodeq2  11340  dvdsle  11555  zsupcllemstep  11651  dvdsbnd  11658  gcdsupex  11659  gcdsupcl  11660  bezoutlemmain  11699  bezoutlemzz  11703  bezoutlembi  11706  dfgcd3  11711  dvdsmulgcd  11726  lcmcllem  11761  lcmgcdlem  11771  ncoprmgcdne1b  11783  pw2dvdslemn  11856  oddpwdclemxy  11860  exmidunben  11952  ctiunctlemfo  11965  unct  11968  tgrest  12354  cnpnei  12404  cnss1  12411  cncnp  12415  ismet2  12539  metequiv2  12681  metcnp  12697  metcnp2  12698  metcnpi3  12702  fsumcncntop  12741  elcncf2  12746  cncfmet  12764  suplociccreex  12787  dedekindicclemicc  12795  ivthinclemlr  12800  ivthinclemur  12802  cnplimclemr  12823  limccnpcntop  12829  limccoap  12832  nninfalllem1  13312  sbthom  13330  apdiff  13350
  Copyright terms: Public domain W3C validator