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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 103 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 458 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:  rmob  2850  isotr  5456  riota5f  5492  tfrexlem  5948  fopwdom  6310  fisbth  6340  fin0  6342  fin0or  6343  diffisn  6350  fientri3  6353  ordiso2  6357  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  ltexnqq  6506  addcmpblnq0  6541  mulcmpblnq0  6542  prmu  6576  addlocpr  6634  prmuloc  6664  prmuloc2  6665  ltaddpr  6695  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  cauappcvgprlemloc  6750  archrecpr  6762  caucvgprlemloc  6773  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  ltsrprg  6832  mulgt0sr  6862  caucvgsrlemgt1  6879  axmulcl  6942  axarch  6965  axcaucvglemres  6973  readdcan  7153  cnegexlem1  7186  negeu  7202  add20  7469  apreap  7578  cru  7593  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  divdivdivap  7689  ltmul12a  7826  lemul12a  7828  lt2mul2div  7845  ledivdiv  7856  lediv12a  7860  qapne  8574  ixxss12  8775  ioodisj  8861  fz0fzelfz0  8984  qtri3or  9098  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  qbtwnre  9111  btwnzge0  9142  expivallem  9256  mulexpzap  9295  leexp1a  9309  expnbnd  9372  cjap  9506  cvg1nlemres  9584  rsqrmo  9625  abs3lem  9707  cau3lem  9710  climcau  9866  qdencn  10124
  Copyright terms: Public domain W3C validator