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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 108 . 2 ((𝜓𝜒) → 𝜒)
21ad2antlr 473 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:  rmob  2920  isotr  5549  riota5f  5586  tfrexlem  6046  tfrcl  6076  nnsucuniel  6203  fopwdom  6497  dif1enen  6541  fisbth  6544  fin0  6546  fin0or  6547  diffisn  6554  finexdc  6563  fientri3  6570  unfidisj  6577  undifdc  6579  ssfirab  6586  fnfi  6589  ordiso2  6664  exmidfodomrlemr  6764  addcmpblnq  6862  mulcmpblnq  6863  ordpipqqs  6869  ltexnqq  6903  addcmpblnq0  6938  mulcmpblnq0  6939  prmu  6973  addlocpr  7031  prmuloc  7061  prmuloc2  7062  ltaddpr  7092  ltexprlemopl  7096  ltexprlemopu  7098  ltexprlemloc  7102  ltexprlemrl  7105  ltexprlemru  7107  addcanprleml  7109  addcanprlemu  7110  aptiprleml  7134  aptiprlemu  7135  ltmprr  7137  cauappcvgprlemloc  7147  archrecpr  7159  caucvgprlemloc  7170  caucvgprprlemloc  7198  caucvgprprlemexbt  7201  addcmpblnr  7221  mulcmpblnrlemg  7222  mulcmpblnr  7223  ltsrprg  7229  mulgt0sr  7259  caucvgsrlemgt1  7276  axmulcl  7339  axarch  7362  axcaucvglemres  7370  readdcan  7558  cnegexlem1  7593  negeu  7609  add20  7888  apreap  7997  cru  8012  apsym  8016  apcotr  8017  apadd1  8018  apneg  8021  mulext1  8022  divdivdivap  8111  ltmul12a  8248  lemul12a  8250  lt2mul2div  8267  ledivdiv  8278  lediv12a  8282  qapne  9048  ixxss12  9248  ioodisj  9334  fz0fzelfz0  9458  qtri3or  9574  exbtwnzlemstep  9579  exbtwnzlemex  9581  exbtwnz  9582  rebtwn2zlemstep  9584  rebtwn2z  9586  qbtwnre  9588  btwnzge0  9627  iseqf1olemqf1o  9818  expivallem  9846  mulexpzap  9885  leexp1a  9900  expnbnd  9965  hashen  10080  fihashdom  10099  hashun  10101  zfz1iso  10134  cjap  10227  cvg1nlemres  10305  rsqrmo  10347  abs3lem  10431  cau3lem  10434  rexanre  10540  climcau  10618  sumeq2  10630  isummo  10654  addmodlteqALT  10726  divalglemeunn  10787  divalglemeuneg  10789  zsupcllemstep  10807  bezoutlemnewy  10851  bezoutlemstep  10852  bezoutlemmain  10853  bezoutlembi  10860  bezoutlemeu  10862  rpdvds  10947  isprm6  10992  pw2dvdslemn  11009  pw2dvdseu  11012  sqrt2irrap  11024  qdencn  11344
  Copyright terms: Public domain W3C validator