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

Theorem simpllr 508
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 479 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  516  f1o2ndf1  6093  tfrlem1  6173  tfr1onlemaccex  6213  tfrcllemaccex  6226  frecabcl  6264  fopwdom  6698  phplem4dom  6724  phpm  6727  phplem4on  6729  fidifsnen  6732  diffisn  6755  diffifi  6756  en2eqpr  6769  fisseneq  6788  suplub2ti  6856  difinfsn  6953  ctmlemr  6961  ctm  6962  ctssdclemn0  6963  ctssdc  6966  enomnilem  6978  addcmpblnq  7143  mulcmpblnq  7144  ordpipqqs  7150  ltexnqq  7184  enq0tr  7210  addcmpblnq0  7219  mulcmpblnq0  7220  nnnq0lem1  7222  prssnqu  7256  prarloclemup  7271  nqprl  7327  nqpru  7328  mullocpr  7347  cauappcvgprlemladdfu  7430  cauappcvgprlemladdrl  7433  caucvgprlemm  7444  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlemlim  7457  caucvgprprlemml  7470  caucvgprprlemloc  7479  caucvgprprlemlim  7487  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  addcmpblnr  7515  mulcmpblnrlemg  7516  mulcmpblnr  7517  ltsrprg  7523  srpospr  7559  caucvgsrlemoffres  7576  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axcaucvglemcau  7674  axsuploc  7805  cnegexlem3  7907  negeu  7921  add20  8204  rimul  8315  apreap  8317  cru  8332  apreim  8333  apsym  8336  apcotr  8337  apadd1  8338  apneg  8341  mulext1  8342  apti  8352  mulap0  8383  prodgt0  8578  ltmul12a  8586  ledivdiv  8616  lediv12a  8620  supinfneg  9358  infsupneg  9359  qapne  9399  xaddf  9595  xaddval  9596  xleadd1a  9624  xleaddadd  9638  ixxss12  9657  ioodisj  9744  fznlem  9789  qtri3or  9988  exbtwnzlemstep  9993  rebtwn2zlemstep  9998  addmodlteq  10139  mulexpzap  10301  leexp1a  10316  expnbnd  10383  faclbnd  10455  hashxp  10540  zfz1iso  10552  cjap  10646  caucvgre  10721  cvg1nlemres  10725  resqrexlemglsq  10762  resqrexlemga  10763  sqrtsq  10784  ltabs  10827  abs3lem  10851  cau3lem  10854  maxleim  10945  rexico  10961  minmax  10969  xrmaxleim  10981  xrmaxiflemcl  10982  xrmaxiflemlub  10985  xrmaxiflemval  10987  xrmaxltsup  10995  xrmaxadd  10998  xrminmax  11002  xrbdtri  11013  climcau  11084  climrecvg1n  11085  sumeq2  11096  summodclem2  11119  divcnv  11234  dvdsle  11469  zsupcllemstep  11565  dvdsbnd  11572  gcdsupex  11573  gcdsupcl  11574  bezoutlemmain  11613  bezoutlemzz  11617  bezoutlembi  11620  dfgcd3  11625  dvdsmulgcd  11640  lcmcllem  11675  lcmgcdlem  11685  ncoprmgcdne1b  11697  pw2dvdslemn  11770  oddpwdclemxy  11774  exmidunben  11866  ctiunctlemfo  11879  unct  11881  tgrest  12265  cnpnei  12315  cnss1  12322  cncnp  12326  ismet2  12450  metequiv2  12592  metcnp  12608  metcnp2  12609  metcnpi3  12613  fsumcncntop  12652  elcncf2  12657  cncfmet  12675  suplociccreex  12698  dedekindicclemicc  12706  ivthinclemlr  12711  ivthinclemur  12713  cnplimclemr  12734  limccnpcntop  12740  limccoap  12743  nninfalllem1  13130  sbthom  13148
  Copyright terms: Public domain W3C validator