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  6425  mulcmpblnq0  6426  prmu  6460  addlocpr  6518  prmuloc  6546  prmuloc2  6547  ltaddpr  6570  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  cauappcvgprlemloc  6623  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  ltsrprg  6655  mulgt0sr  6684  axmulcl  6732  axarch  6753  readdcan  6930  cnegexlem1  6963  negeu  6979  add20  7244  apreap  7351  cru  7366  apsym  7370  apcotr  7371  apadd1  7372  apneg  7375  mulext1  7376  divdivdivap  7451  ltmul12a  7587  lemul12a  7589  lt2mul2div  7606  ledivdiv  7617  lediv12a  7621  qapne  8330  ixxss12  8525  ioodisj  8611  fz0fzelfz0  8734  expivallem  8890  mulexpzap  8929  leexp1a  8943  expnbnd  9005  cjap  9114
  Copyright terms: Public domain W3C validator