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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 108 . 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:  fliftfun  5467  grpridd  5728  tfrlemisucaccv  5974  tfr1onlemsucaccv  5990  tfrcllemsucaccv  6003  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  nqnq0pi  6690  addcmpblnq0  6695  mulcmpblnq0  6696  addnq0mo  6699  mulnq0mo  6700  prarloclemcalc  6754  prarloc  6755  nqprl  6803  mullocpr  6823  distrlem4prl  6836  distrlem4pru  6837  ltprordil  6841  ltexprlemlol  6854  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  addsrmo  6982  mulsrmo  6983  ltsrprg  6986  axmulcl  7096  recriota  7118  ltmul1  7759  divdivdivap  7868  divsubdivap  7883  ledivdiv  8035  lediv12a  8039  exbtwnz  9337  qbtwnre  9343  ioom  9347  iseqcaopr  9558  leexp2r  9627  sizeunlem  9828  recvguniq  10019  rsqrmo  10051  bezout  10544  qredeu  10623  pw2dvdseu  10690  oddpwdclemndvds  10693
  Copyright terms: Public domain W3C validator