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

Theorem simplrr 488
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrr (((φ (ψ χ)) θ) → χ)

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 103 . 2 ((ψ χ) → χ)
21ad2antlr 458 1 (((φ (ψ χ)) θ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  rmob  2844  isotr  5399  riota5f  5435  tfrexlem  5889  fopwdom  6246  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  ltexnqq  6391  addcmpblnq0  6426  mulcmpblnq0  6427  prmu  6461  addlocpr  6519  prmuloc  6547  prmuloc2  6548  ltaddpr  6571  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  cauappcvgprlemloc  6624  caucvgprlemloc  6646  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  ltsrprg  6675  mulgt0sr  6704  axmulcl  6752  axarch  6773  readdcan  6950  cnegexlem1  6983  negeu  6999  add20  7264  apreap  7371  cru  7386  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  divdivdivap  7471  ltmul12a  7607  lemul12a  7609  lt2mul2div  7626  ledivdiv  7637  lediv12a  7641  qapne  8350  ixxss12  8545  ioodisj  8631  fz0fzelfz0  8754  expivallem  8910  mulexpzap  8949  leexp1a  8963  expnbnd  9025  cjap  9134
  Copyright terms: Public domain W3C validator