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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 102 . 2 ((χ θ) → χ)
21ad2antll 460 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:  dn1dc  866  imain  4924  grpridd  5639  tfrlemisucaccv  5880  tfrexlem  5889  eroveu  6133  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  nqnq0pi  6421  addcmpblnq0  6426  mulcmpblnq0  6427  prarloclemcalc  6485  prarloc  6486  mullocpr  6552  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  ltexprlemm  6574  ltexprlemopu  6577  ltexprlemupu  6578  ltexprlemru  6586  cauappcvgprlemopl  6618  cauappcvgprlem2  6632  caucvgprlemopl  6640  caucvgprlem2  6651  addcmpblnr  6667  mulcmpblnrlemg  6668  mulcmpblnr  6669  prsrlem1  6670  ltsrprg  6675  axmulcl  6752  ltmul1  7376  divdivdivap  7471  divmuleqap  7475  divsubdivap  7486  lt2mul2div  7626  ledivdiv  7637  lediv12a  7641  ssfzo12bi  8851  leexp2r  8962
  Copyright terms: Public domain W3C validator