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

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

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 108 . 2 ((𝜑𝜓) → 𝜓)
21ad2antrr 472 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  simp-4r  509  f1o2ndf1  5952  tfrlem1  6029  tfr1onlemaccex  6069  tfrcllemaccex  6082  frecabcl  6120  fopwdom  6506  phplem4dom  6532  phpm  6535  phplem4on  6537  fidifsnen  6540  diffisn  6563  diffifi  6564  en2eqpr  6577  fisseneq  6595  suplub2ti  6643  enomnilem  6741  addcmpblnq  6873  mulcmpblnq  6874  ordpipqqs  6880  ltexnqq  6914  enq0tr  6940  addcmpblnq0  6949  mulcmpblnq0  6950  nnnq0lem1  6952  prssnqu  6986  prarloclemup  7001  nqprl  7057  nqpru  7058  mullocpr  7077  cauappcvgprlemladdfu  7160  cauappcvgprlemladdrl  7163  caucvgprlemm  7174  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlemlim  7187  caucvgprprlemml  7200  caucvgprprlemloc  7209  caucvgprprlemlim  7217  addcmpblnr  7232  mulcmpblnrlemg  7233  mulcmpblnr  7234  ltsrprg  7240  srpospr  7275  caucvgsrlemoffres  7292  axcaucvglemcau  7380  cnegexlem3  7606  negeu  7620  add20  7899  rimul  8006  apreap  8008  cru  8023  apreim  8024  apsym  8027  apcotr  8028  apadd1  8029  apneg  8032  mulext1  8033  apti  8043  mulap0  8065  prodgt0  8251  ltmul12a  8259  ledivdiv  8289  lediv12a  8293  supinfneg  9018  infsupneg  9019  qapne  9059  ixxss12  9259  ioodisj  9345  fznlem  9390  qtri3or  9585  exbtwnzlemstep  9590  rebtwn2zlemstep  9595  addmodlteq  9736  mulexpzap  9897  leexp1a  9912  expnbnd  9977  faclbnd  10049  hashxp  10134  zfz1iso  10146  cjap  10239  caucvgre  10313  cvg1nlemres  10317  resqrexlemglsq  10354  resqrexlemga  10355  sqrtsq  10376  ltabs  10419  abs3lem  10443  cau3lem  10446  maxleim  10537  rexico  10553  minmax  10559  climcau  10631  climrecvg1n  10632  sumeq2  10643  isummolem2  10666  dvdsle  10751  zsupcllemstep  10847  dvdsbnd  10854  gcdsupex  10855  gcdsupcl  10856  bezoutlemmain  10893  bezoutlemzz  10897  bezoutlembi  10900  dfgcd3  10905  dvdsmulgcd  10920  lcmcllem  10955  lcmgcdlem  10965  ncoprmgcdne1b  10977  pw2dvdslemn  11049  oddpwdclemxy  11053  nninfalllem1  11368
  Copyright terms: Public domain W3C validator