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

Theorem simprrl 506
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprrl ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 107 . 2 ((𝜒𝜃) → 𝜒)
21ad2antll 475 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  dn1dc  902  imain  5012  grpridd  5728  tfrlemisucaccv  5974  tfrexlem  5983  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  eroveu  6263  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  nqnq0pi  6690  addcmpblnq0  6695  mulcmpblnq0  6696  prarloclemcalc  6754  prarloc  6755  nqpru  6804  mullocpr  6823  distrlem4prl  6836  distrlem4pru  6837  ltprordil  6841  ltexprlemm  6852  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemru  6864  cauappcvgprlemopl  6898  cauappcvgprlem2  6912  caucvgprlemopl  6921  caucvgprlem2  6932  caucvgprprlemexbt  6958  caucvgprprlem2  6962  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  prsrlem1  6981  ltsrprg  6986  axmulcl  7096  ltmul1  7759  divdivdivap  7868  divmuleqap  7872  divsubdivap  7883  lt2mul2div  8024  ledivdiv  8035  lediv12a  8039  ssfzo12bi  9311  exbtwnz  9337  qbtwnre  9343  ioom  9347  iseqcaopr  9558  leexp2r  9627  sizeunlem  9828  recvguniq  10019  rsqrmo  10051  bezout  10544  qredeu  10623  pw2dvdseu  10690  oddpwdclemdvds  10692
  Copyright terms: Public domain W3C validator