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  8314  apreap  8316  cru  8331  apreim  8332  apsym  8335  apcotr  8336  apadd1  8337  apneg  8340  mulext1  8341  apti  8351  mulap0  8382  prodgt0  8574  ltmul12a  8582  ledivdiv  8612  lediv12a  8616  supinfneg  9346  infsupneg  9347  qapne  9387  xaddf  9582  xaddval  9583  xleadd1a  9611  xleaddadd  9625  ixxss12  9644  ioodisj  9731  fznlem  9776  qtri3or  9975  exbtwnzlemstep  9980  rebtwn2zlemstep  9985  addmodlteq  10126  mulexpzap  10288  leexp1a  10303  expnbnd  10370  faclbnd  10442  hashxp  10527  zfz1iso  10539  cjap  10633  caucvgre  10708  cvg1nlemres  10712  resqrexlemglsq  10749  resqrexlemga  10750  sqrtsq  10771  ltabs  10814  abs3lem  10838  cau3lem  10841  maxleim  10932  rexico  10948  minmax  10956  xrmaxleim  10968  xrmaxiflemcl  10969  xrmaxiflemlub  10972  xrmaxiflemval  10974  xrmaxltsup  10982  xrmaxadd  10985  xrminmax  10989  xrbdtri  11000  climcau  11071  climrecvg1n  11072  sumeq2  11083  summodclem2  11106  divcnv  11221  dvdsle  11454  zsupcllemstep  11550  dvdsbnd  11557  gcdsupex  11558  gcdsupcl  11559  bezoutlemmain  11598  bezoutlemzz  11602  bezoutlembi  11605  dfgcd3  11610  dvdsmulgcd  11625  lcmcllem  11660  lcmgcdlem  11670  ncoprmgcdne1b  11682  pw2dvdslemn  11754  oddpwdclemxy  11758  exmidunben  11850  ctiunctlemfo  11863  unct  11865  tgrest  12249  cnpnei  12299  cnss1  12306  cncnp  12310  ismet2  12434  metequiv2  12576  metcnp  12592  metcnp2  12593  metcnpi3  12597  fsumcncntop  12636  elcncf2  12641  cncfmet  12659  suplociccreex  12682  dedekindicclemicc  12690  ivthinclemlr  12695  ivthinclemur  12697  cnplimclemr  12718  limccnpcntop  12724  limccoap  12727  nninfalllem1  13099  sbthom  13117
  Copyright terms: Public domain W3C validator