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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 108 . 2 ((𝜓𝜒) → 𝜓)
21ad2antlr 481 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  rmob  3004  disjiun  3931  f1imass  5682  riota5f  5761  tfrexlem  6238  tfrcl  6268  nnsucuniel  6398  nntr2  6406  fopwdom  6737  fidceq  6770  fisbth  6784  fientri3  6810  unsnfidcex  6815  undifdc  6819  iunfidisj  6841  fiuni  6873  ordiso2  6927  acfun  7079  ccfunen  7095  addcmpblnq  7198  mulcmpblnq  7199  ordpipqqs  7205  addcmpblnq0  7274  mulcmpblnq0  7275  prml  7308  addlocpr  7367  prmuloc  7397  mullocpr  7402  ltexprlemopl  7432  ltexprlemopu  7434  ltexprlemloc  7438  ltexprlemrl  7441  ltexprlemru  7443  addcanprleml  7445  addcanprlemu  7446  aptiprleml  7470  ltmprr  7473  cauappcvgprlemopl  7477  cauappcvgprlemopu  7479  cauappcvgprlemloc  7483  caucvgprlemopl  7500  caucvgprlemopu  7502  caucvgprlemloc  7506  caucvgprprlemopu  7530  caucvgprprlemloc  7534  caucvgprprlemexbt  7537  caucvgprprlemaddq  7539  suplocexprlemrl  7548  suplocexprlemdisj  7551  suplocexprlemloc  7552  suplocexprlemub  7554  addcmpblnr  7570  mulcmpblnrlemg  7571  mulcmpblnr  7572  ltsrprg  7578  mulgt0sr  7609  caucvgsrlemgt1  7626  suplocsrlemb  7637  axmulcl  7697  axcaucvglemres  7730  axpre-suploclemres  7732  axpre-suploc  7733  cnegexlem1  7960  negeu  7976  add20  8259  apreap  8372  cru  8387  apsym  8391  apcotr  8392  apadd1  8393  apneg  8396  mulext1  8397  mulge0  8404  mulap0  8438  divdivdivap  8496  prodgt0  8633  ltmul12a  8641  lt2mul2div  8660  ledivdiv  8671  lediv12a  8675  qapne  9457  xleadd1a  9685  ixxss12  9718  elfz0ubfz0  9932  qtri3or  10050  exbtwnzlemstep  10055  exbtwnzlemex  10057  exbtwnz  10058  rebtwn2zlemstep  10060  rebtwn2z  10062  btwnzge0  10103  iseqf1olemqf1o  10296  mulexpzap  10363  leexp1a  10378  hashen  10561  fihashdom  10580  hashun  10582  cjap  10709  cvg1nlemres  10788  rsqrmo  10830  abslt  10891  abs3lem  10914  cau3lem  10917  rexanre  11023  xrmaxltsup  11058  climcau  11147  sumeq2  11159  summodc  11183  fisumss  11192  fsum2d  11235  fsumabs  11265  fsumiun  11277  prodeq2  11357  prodmodclem2  11377  eirrap  11518  divalglemeunn  11652  divalglemeuneg  11654  bezoutlemnewy  11718  bezoutlemstep  11719  bezoutlemmain  11720  bezoutlembi  11727  bezoutlemeu  11729  qredeu  11812  pw2dvdseu  11880  sqrt2irrap  11892  ennnfonelemg  11950  ennnfonelemrnh  11963  ctiunctlemfo  11986  restbasg  12374  cnpnei  12425  cnptoprest2  12446  cnpdis  12448  lmtopcnp  12456  txcnp  12477  ismet2  12560  blininf  12630  metss2lem  12703  xmettxlem  12715  xmettx  12716  metcnp  12718  metcnpi3  12723  addcncntoplem  12757  fsumcncntop  12762  mulc1cncf  12782  cncfco  12784  mulcncf  12797  dedekindeulemuub  12801  dedekindeu  12807  dedekindicclemuub  12810  ivthinclemloc  12825  ivthinc  12827  limcimo  12840  limccnp2cntop  12852  dveflem  12893  logbgcd1irrap  13093  qdencn  13395  apdiff  13414
  Copyright terms: Public domain W3C validator