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

Theorem simplrr 508
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 478 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  2971  disjiun  3892  isotr  5683  riota5f  5720  tfrexlem  6197  tfrcl  6227  nnsucuniel  6357  fopwdom  6696  dif1enen  6740  fisbth  6743  fin0  6745  fin0or  6746  diffisn  6753  finexdc  6762  fientri3  6769  unfidisj  6776  undifdc  6778  ssfirab  6788  fnfi  6791  iunfidisj  6800  ordiso2  6886  difinfinf  6952  ctmlemr  6959  exmidfodomrlemr  7022  addcmpblnq  7139  mulcmpblnq  7140  ordpipqqs  7146  ltexnqq  7180  addcmpblnq0  7215  mulcmpblnq0  7216  prmu  7250  addlocpr  7308  prmuloc  7338  prmuloc2  7339  ltaddpr  7369  ltexprlemopl  7373  ltexprlemopu  7375  ltexprlemloc  7379  ltexprlemrl  7382  ltexprlemru  7384  addcanprleml  7386  addcanprlemu  7387  aptiprleml  7411  aptiprlemu  7412  ltmprr  7414  cauappcvgprlemloc  7424  archrecpr  7436  caucvgprlemloc  7447  caucvgprprlemloc  7475  caucvgprprlemexbt  7478  suplocexprlemdisj  7492  suplocexprlemloc  7493  addcmpblnr  7511  mulcmpblnrlemg  7512  mulcmpblnr  7513  ltsrprg  7519  mulgt0sr  7550  caucvgsrlemgt1  7567  suplocsrlemb  7578  axmulcl  7638  axarch  7663  axcaucvglemres  7671  axpre-suploclemres  7673  axpre-suploc  7674  readdcan  7866  cnegexlem1  7901  negeu  7917  add20  8200  apreap  8312  cru  8327  apsym  8331  apcotr  8332  apadd1  8333  apneg  8336  mulext1  8337  divdivdivap  8436  ltmul12a  8578  lemul12a  8580  lt2mul2div  8597  ledivdiv  8608  lediv12a  8612  qapne  9383  xleadd1a  9607  ixxss12  9640  ioodisj  9727  fz0fzelfz0  9855  qtri3or  9971  exbtwnzlemstep  9976  exbtwnzlemex  9978  exbtwnz  9979  rebtwn2zlemstep  9981  rebtwn2z  9983  qbtwnre  9985  btwnzge0  10024  iseqf1olemqf1o  10217  mulexpzap  10284  leexp1a  10299  expnbnd  10366  hashen  10481  fihashdom  10500  hashun  10502  zfz1iso  10535  cjap  10629  cvg1nlemres  10708  rsqrmo  10750  abs3lem  10834  cau3lem  10837  rexanre  10943  xrmaxltsup  10978  climcau  11067  sumeq2  11079  summodc  11103  fsum3cvg3  11116  fsum2d  11155  eirrap  11391  addmodlteqALT  11464  divalglemeunn  11525  divalglemeuneg  11527  zsupcllemstep  11545  bezoutlemnewy  11591  bezoutlemstep  11592  bezoutlemmain  11593  bezoutlembi  11600  bezoutlemeu  11602  rpdvds  11687  isprm6  11732  pw2dvdslemn  11749  pw2dvdseu  11752  sqrt2irrap  11764  ennnfonelemrnh  11835  ennnfonelemnn0  11841  ctinfomlemom  11846  ctiunctlemfo  11858  restbasg  12243  cnrest2  12311  cnpdis  12317  lmtopcnp  12325  txcnp  12346  txlm  12354  ismet2  12429  blininf  12499  metss2lem  12572  xmettxlem  12584  xmettx  12585  metcnp3  12586  metcnpi3  12592  addcncntoplem  12626  fsumcncntop  12631  mulcncf  12666  dedekindeulemuub  12670  dedekindeu  12676  dedekindicclemuub  12679  ivthinclemlopn  12689  ivthinclemuopn  12691  ivthinclemloc  12694  ivthinc  12696  limcimo  12709  limccnp2cntop  12721  qdencn  13056
  Copyright terms: Public domain W3C validator