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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 102 . 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  f1imass  5413  riota5f  5492  tfrexlem  5948  fopwdom  6310  fidceq  6330  fisbth  6340  fientri3  6353  ordiso2  6355  addcmpblnq  6463  mulcmpblnq  6464  ordpipqqs  6470  addcmpblnq0  6539  mulcmpblnq0  6540  prml  6573  addlocpr  6632  prmuloc  6662  mullocpr  6667  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemloc  6703  ltexprlemrl  6706  ltexprlemru  6708  addcanprleml  6710  addcanprlemu  6711  aptiprleml  6735  ltmprr  6738  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemloc  6748  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemloc  6771  caucvgprprlemopu  6795  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemaddq  6804  addcmpblnr  6822  mulcmpblnrlemg  6823  mulcmpblnr  6824  ltsrprg  6830  mulgt0sr  6860  caucvgsrlemgt1  6877  axmulcl  6940  axcaucvglemres  6971  cnegexlem1  7184  negeu  7200  add20  7467  apreap  7576  cru  7591  apsym  7595  apcotr  7596  apadd1  7597  apneg  7600  mulext1  7601  mulge0  7608  mulap0  7633  divdivdivap  7687  prodgt0  7816  ltmul12a  7824  lt2mul2div  7843  ledivdiv  7854  lediv12a  7858  qapne  8572  ixxss12  8773  elfz0ubfz0  8980  qtri3or  9096  qbtwnzlemstep  9101  qbtwnzlemex  9103  qbtwnz  9104  rebtwn2zlemstep  9105  rebtwn2z  9107  btwnzge0  9140  expivallem  9230  mulexpzap  9269  leexp1a  9283  cjap  9480  cvg1nlemres  9558  rsqrmo  9599  abslt  9658  abs3lem  9681  cau3lem  9684  climcau  9840  qdencn  10097
  Copyright terms: Public domain W3C validator