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

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

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 109 . 2 ((𝜑𝜓) → 𝜓)
21ad2antrr 480 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:  simp-4r  532  f1o2ndf1  6132  tfrlem1  6212  tfr1onlemaccex  6252  tfrcllemaccex  6265  frecabcl  6303  fopwdom  6737  phplem4dom  6763  phpm  6766  phplem4on  6768  fidifsnen  6771  diffisn  6794  diffifi  6795  en2eqpr  6808  fisseneq  6827  suplub2ti  6895  difinfsn  6992  ctmlemr  7000  ctm  7001  ctssdclemn0  7002  ctssdc  7005  enomnilem  7017  enmkvlem  7042  enwomnilem  7049  cc3  7099  addcmpblnq  7198  mulcmpblnq  7199  ordpipqqs  7205  ltexnqq  7239  enq0tr  7265  addcmpblnq0  7274  mulcmpblnq0  7275  nnnq0lem1  7277  prssnqu  7311  prarloclemup  7326  nqprl  7382  nqpru  7383  mullocpr  7402  cauappcvgprlemladdfu  7485  cauappcvgprlemladdrl  7488  caucvgprlemm  7499  caucvgprlemladdfu  7508  caucvgprlemladdrl  7509  caucvgprlemlim  7512  caucvgprprlemml  7525  caucvgprprlemloc  7534  caucvgprprlemlim  7542  suplocexprlemmu  7549  suplocexprlemru  7550  suplocexprlemdisj  7551  suplocexprlemloc  7552  addcmpblnr  7570  mulcmpblnrlemg  7571  mulcmpblnr  7572  ltsrprg  7578  srpospr  7614  caucvgsrlemoffres  7631  suplocsrlemb  7637  suplocsrlempr  7638  suplocsrlem  7639  axcaucvglemcau  7729  axsuploc  7860  cnegexlem3  7962  negeu  7976  add20  8259  rimul  8370  apreap  8372  cru  8387  apreim  8388  apsym  8391  apcotr  8392  apadd1  8393  apneg  8396  mulext1  8397  apti  8407  mulap0  8438  prodgt0  8633  ltmul12a  8641  ledivdiv  8671  lediv12a  8675  supinfneg  9416  infsupneg  9417  qapne  9457  xaddf  9656  xaddval  9657  xleadd1a  9685  xleaddadd  9699  ixxss12  9718  ioodisj  9805  fznlem  9851  qtri3or  10050  exbtwnzlemstep  10055  rebtwn2zlemstep  10060  addmodlteq  10201  mulexpzap  10363  leexp1a  10378  expnbnd  10445  apexp1  10495  faclbnd  10518  hashxp  10603  zfz1iso  10615  cjap  10709  caucvgre  10784  cvg1nlemres  10788  resqrexlemglsq  10825  resqrexlemga  10826  sqrtsq  10847  ltabs  10890  abs3lem  10914  cau3lem  10917  maxleim  11008  rexico  11024  minmax  11032  xrmaxleim  11044  xrmaxiflemcl  11045  xrmaxiflemlub  11048  xrmaxiflemval  11050  xrmaxltsup  11058  xrmaxadd  11061  xrminmax  11065  xrbdtri  11076  climcau  11147  climrecvg1n  11148  sumeq2  11159  summodclem2  11182  divcnv  11297  prodeq2  11357  dvdsle  11576  zsupcllemstep  11672  dvdsbnd  11679  gcdsupex  11680  gcdsupcl  11681  bezoutlemmain  11720  bezoutlemzz  11724  bezoutlembi  11727  dfgcd3  11732  dvdsmulgcd  11747  lcmcllem  11782  lcmgcdlem  11792  ncoprmgcdne1b  11804  pw2dvdslemn  11877  oddpwdclemxy  11881  exmidunben  11973  ctiunctlemfo  11986  unct  11989  tgrest  12375  cnpnei  12425  cnss1  12432  cncnp  12436  ismet2  12560  metequiv2  12702  metcnp  12718  metcnp2  12719  metcnpi3  12723  fsumcncntop  12762  elcncf2  12767  cncfmet  12785  suplociccreex  12808  dedekindicclemicc  12816  ivthinclemlr  12821  ivthinclemur  12823  cnplimclemr  12844  limccnpcntop  12850  limccoap  12853  nninfalllem1  13376  sbthom  13394  apdiff  13414
  Copyright terms: Public domain W3C validator