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  904  imain  5061  grpridd  5798  tfrlemisucaccv  6044  tfrexlem  6053  tfr1onlemsucaccv  6060  tfrcllemsucaccv  6073  eroveu  6335  addcmpblnq  6870  mulcmpblnq  6871  ordpipqqs  6877  nqnq0pi  6941  addcmpblnq0  6946  mulcmpblnq0  6947  prarloclemcalc  7005  prarloc  7006  nqpru  7055  mullocpr  7074  distrlem4prl  7087  distrlem4pru  7088  ltprordil  7092  ltexprlemm  7103  ltexprlemopu  7106  ltexprlemupu  7107  ltexprlemru  7115  cauappcvgprlemopl  7149  cauappcvgprlem2  7163  caucvgprlemopl  7172  caucvgprlem2  7183  caucvgprprlemexbt  7209  caucvgprprlem2  7213  addcmpblnr  7229  mulcmpblnrlemg  7230  mulcmpblnr  7231  prsrlem1  7232  ltsrprg  7237  axmulcl  7347  ltmul1  8010  divdivdivap  8119  divmuleqap  8123  divsubdivap  8134  lt2mul2div  8275  ledivdiv  8286  lediv12a  8290  ssfzo12bi  9564  exbtwnz  9590  qbtwnre  9596  ioom  9600  iseqcaopr  9817  leexp2r  9908  hashunlem  10109  recvguniq  10324  rsqrmo  10356  bezout  10882  qredeu  10961  pw2dvdseu  11028  oddpwdclemdvds  11030
  Copyright terms: Public domain W3C validator