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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 108 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antlr 480 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:  rmob  3001  disjiun  3924  f1imass  5675  riota5f  5754  tfrexlem  6231  tfrcl  6261  nnsucuniel  6391  nntr2  6399  fopwdom  6730  fidceq  6763  fisbth  6777  fientri3  6803  unsnfidcex  6808  undifdc  6812  iunfidisj  6834  fiuni  6866  ordiso2  6920  acfun  7068  ccfunen  7084  addcmpblnq  7187  mulcmpblnq  7188  ordpipqqs  7194  addcmpblnq0  7263  mulcmpblnq0  7264  prml  7297  addlocpr  7356  prmuloc  7386  mullocpr  7391  ltexprlemopl  7421  ltexprlemopu  7423  ltexprlemloc  7427  ltexprlemrl  7430  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  aptiprleml  7459  ltmprr  7462  cauappcvgprlemopl  7466  cauappcvgprlemopu  7468  cauappcvgprlemloc  7472  caucvgprlemopl  7489  caucvgprlemopu  7491  caucvgprlemloc  7495  caucvgprprlemopu  7519  caucvgprprlemloc  7523  caucvgprprlemexbt  7526  caucvgprprlemaddq  7528  suplocexprlemrl  7537  suplocexprlemdisj  7540  suplocexprlemloc  7541  suplocexprlemub  7543  addcmpblnr  7559  mulcmpblnrlemg  7560  mulcmpblnr  7561  ltsrprg  7567  mulgt0sr  7598  caucvgsrlemgt1  7615  suplocsrlemb  7626  axmulcl  7686  axcaucvglemres  7719  axpre-suploclemres  7721  axpre-suploc  7722  cnegexlem1  7949  negeu  7965  add20  8248  apreap  8361  cru  8376  apsym  8380  apcotr  8381  apadd1  8382  apneg  8385  mulext1  8386  mulge0  8393  mulap0  8427  divdivdivap  8485  prodgt0  8622  ltmul12a  8630  lt2mul2div  8649  ledivdiv  8660  lediv12a  8664  qapne  9443  xleadd1a  9668  ixxss12  9701  elfz0ubfz0  9914  qtri3or  10032  exbtwnzlemstep  10037  exbtwnzlemex  10039  exbtwnz  10040  rebtwn2zlemstep  10042  rebtwn2z  10044  btwnzge0  10085  iseqf1olemqf1o  10278  mulexpzap  10345  leexp1a  10360  hashen  10542  fihashdom  10561  hashun  10563  cjap  10690  cvg1nlemres  10769  rsqrmo  10811  abslt  10872  abs3lem  10895  cau3lem  10898  rexanre  11004  xrmaxltsup  11039  climcau  11128  sumeq2  11140  summodc  11164  fisumss  11173  fsum2d  11216  fsumabs  11246  fsumiun  11258  prodeq2  11338  prodmodclem2  11358  eirrap  11495  divalglemeunn  11629  divalglemeuneg  11631  bezoutlemnewy  11695  bezoutlemstep  11696  bezoutlemmain  11697  bezoutlembi  11704  bezoutlemeu  11706  qredeu  11789  pw2dvdseu  11857  sqrt2irrap  11869  ennnfonelemg  11927  ennnfonelemrnh  11940  ctiunctlemfo  11963  restbasg  12351  cnpnei  12402  cnptoprest2  12423  cnpdis  12425  lmtopcnp  12433  txcnp  12454  ismet2  12537  blininf  12607  metss2lem  12680  xmettxlem  12692  xmettx  12693  metcnp  12695  metcnpi3  12700  addcncntoplem  12734  fsumcncntop  12739  mulc1cncf  12759  cncfco  12761  mulcncf  12774  dedekindeulemuub  12778  dedekindeu  12784  dedekindicclemuub  12787  ivthinclemloc  12802  ivthinc  12804  limcimo  12817  limccnp2cntop  12829  dveflem  12870  qdencn  13283  apdiff  13300
  Copyright terms: Public domain W3C validator