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  6420  addcmpblnq0  6425  mulcmpblnq0  6426  prarloclemcalc  6484  prarloc  6485  mullocpr  6551  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  ltexprlemm  6573  ltexprlemopu  6576  ltexprlemupu  6577  ltexprlemru  6585  cauappcvgprlemopl  6617  cauappcvgprlem2  6631  addcmpblnr  6647  mulcmpblnrlemg  6648  mulcmpblnr  6649  prsrlem1  6650  ltsrprg  6655  axmulcl  6732  ltmul1  7356  divdivdivap  7451  divmuleqap  7455  divsubdivap  7466  lt2mul2div  7606  ledivdiv  7617  lediv12a  7621  ssfzo12bi  8831  leexp2r  8942
  Copyright terms: Public domain W3C validator