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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 109 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 480 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
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:  rmob  2973  disjiun  3894  isotr  5685  riota5f  5722  tfrexlem  6199  tfrcl  6229  nnsucuniel  6359  fopwdom  6698  dif1enen  6742  fisbth  6745  fin0  6747  fin0or  6748  diffisn  6755  finexdc  6764  fientri3  6771  unfidisj  6778  undifdc  6780  ssfirab  6790  fnfi  6793  iunfidisj  6802  ordiso2  6888  difinfinf  6954  ctmlemr  6961  exmidfodomrlemr  7026  addcmpblnq  7143  mulcmpblnq  7144  ordpipqqs  7150  ltexnqq  7184  addcmpblnq0  7219  mulcmpblnq0  7220  prmu  7254  addlocpr  7312  prmuloc  7342  prmuloc2  7343  ltaddpr  7373  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  aptiprleml  7415  aptiprlemu  7416  ltmprr  7418  cauappcvgprlemloc  7428  archrecpr  7440  caucvgprlemloc  7451  caucvgprprlemloc  7479  caucvgprprlemexbt  7482  suplocexprlemdisj  7496  suplocexprlemloc  7497  addcmpblnr  7515  mulcmpblnrlemg  7516  mulcmpblnr  7517  ltsrprg  7523  mulgt0sr  7554  caucvgsrlemgt1  7571  suplocsrlemb  7582  axmulcl  7642  axarch  7667  axcaucvglemres  7675  axpre-suploclemres  7677  axpre-suploc  7678  readdcan  7870  cnegexlem1  7905  negeu  7921  add20  8204  apreap  8316  cru  8331  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  divdivdivap  8440  ltmul12a  8582  lemul12a  8584  lt2mul2div  8601  ledivdiv  8612  lediv12a  8616  qapne  9387  xleadd1a  9611  ixxss12  9644  ioodisj  9731  fz0fzelfz0  9859  qtri3or  9975  exbtwnzlemstep  9980  exbtwnzlemex  9982  exbtwnz  9983  rebtwn2zlemstep  9985  rebtwn2z  9987  qbtwnre  9989  btwnzge0  10028  iseqf1olemqf1o  10221  mulexpzap  10288  leexp1a  10303  expnbnd  10370  hashen  10485  fihashdom  10504  hashun  10506  zfz1iso  10539  cjap  10633  cvg1nlemres  10712  rsqrmo  10754  abs3lem  10838  cau3lem  10841  rexanre  10947  xrmaxltsup  10982  climcau  11071  sumeq2  11083  summodc  11107  fsum3cvg3  11120  fsum2d  11159  eirrap  11396  addmodlteqALT  11469  divalglemeunn  11530  divalglemeuneg  11532  zsupcllemstep  11550  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlembi  11605  bezoutlemeu  11607  rpdvds  11692  isprm6  11737  pw2dvdslemn  11754  pw2dvdseu  11757  sqrt2irrap  11769  ennnfonelemrnh  11840  ennnfonelemnn0  11846  ctinfomlemom  11851  ctiunctlemfo  11863  restbasg  12248  cnrest2  12316  cnpdis  12322  lmtopcnp  12330  txcnp  12351  txlm  12359  ismet2  12434  blininf  12504  metss2lem  12577  xmettxlem  12589  xmettx  12590  metcnp3  12591  metcnpi3  12597  addcncntoplem  12631  fsumcncntop  12636  mulcncf  12671  dedekindeulemuub  12675  dedekindeu  12681  dedekindicclemuub  12684  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthinclemloc  12699  ivthinc  12701  limcimo  12714  limccnp2cntop  12726  qdencn  13118
  Copyright terms: Public domain W3C validator