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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 107 . 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  f1imass  5514  riota5f  5593  tfrexlem  6053  tfrcl  6083  nnsucuniel  6210  fopwdom  6504  fidceq  6537  fisbth  6551  fientri3  6577  unsnfidcex  6582  undifdc  6586  ordiso2  6672  addcmpblnq  6870  mulcmpblnq  6871  ordpipqqs  6877  addcmpblnq0  6946  mulcmpblnq0  6947  prml  6980  addlocpr  7039  prmuloc  7069  mullocpr  7074  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemloc  7110  ltexprlemrl  7113  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  aptiprleml  7142  ltmprr  7145  cauappcvgprlemopl  7149  cauappcvgprlemopu  7151  cauappcvgprlemloc  7155  caucvgprlemopl  7172  caucvgprlemopu  7174  caucvgprlemloc  7178  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemaddq  7211  addcmpblnr  7229  mulcmpblnrlemg  7230  mulcmpblnr  7231  ltsrprg  7237  mulgt0sr  7267  caucvgsrlemgt1  7284  axmulcl  7347  axcaucvglemres  7378  cnegexlem1  7601  negeu  7617  add20  7896  apreap  8005  cru  8020  apsym  8024  apcotr  8025  apadd1  8026  apneg  8029  mulext1  8030  mulge0  8037  mulap0  8062  divdivdivap  8119  prodgt0  8248  ltmul12a  8256  lt2mul2div  8275  ledivdiv  8286  lediv12a  8290  qapne  9056  ixxss12  9256  elfz0ubfz0  9464  qtri3or  9582  exbtwnzlemstep  9587  exbtwnzlemex  9589  exbtwnz  9590  rebtwn2zlemstep  9592  rebtwn2z  9594  btwnzge0  9635  iseqf1olemqf1o  9827  expivallem  9855  mulexpzap  9894  leexp1a  9909  hashen  10089  fihashdom  10108  hashun  10110  cjap  10236  cvg1nlemres  10314  rsqrmo  10356  abslt  10417  abs3lem  10440  cau3lem  10443  rexanre  10549  climcau  10628  sumeq2  10640  isummo  10664  fisumss  10672  divalglemeunn  10803  divalglemeuneg  10805  bezoutlemnewy  10867  bezoutlemstep  10868  bezoutlemmain  10869  bezoutlembi  10876  bezoutlemeu  10878  qredeu  10961  pw2dvdseu  11028  sqrt2irrap  11040  qdencn  11360
  Copyright terms: Public domain W3C validator