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  5880  tfrlem1  5957  tfr1onlemaccex  5997  tfrcllemaccex  6010  frecabcl  6048  fopwdom  6380  phplem4dom  6397  phpm  6400  phplem4on  6402  fidifsnen  6405  diffisn  6427  diffifi  6428  en2eqpr  6434  suplub2ti  6473  addcmpblnq  6619  mulcmpblnq  6620  ordpipqqs  6626  ltexnqq  6660  enq0tr  6686  addcmpblnq0  6695  mulcmpblnq0  6696  nnnq0lem1  6698  prssnqu  6732  prarloclemup  6747  nqprl  6803  nqpru  6804  mullocpr  6823  cauappcvgprlemladdfu  6906  cauappcvgprlemladdrl  6909  caucvgprlemm  6920  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlemlim  6933  caucvgprprlemml  6946  caucvgprprlemloc  6955  caucvgprprlemlim  6963  addcmpblnr  6978  mulcmpblnrlemg  6979  mulcmpblnr  6980  ltsrprg  6986  srpospr  7021  caucvgsrlemoffres  7038  axcaucvglemcau  7126  cnegexlem3  7352  negeu  7366  add20  7645  rimul  7752  apreap  7754  cru  7769  apreim  7770  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  apti  7789  mulap0  7811  prodgt0  7997  ltmul12a  8005  ledivdiv  8035  lediv12a  8039  supinfneg  8764  infsupneg  8765  qapne  8805  ixxss12  9005  ioodisj  9091  fznlem  9136  qtri3or  9329  exbtwnzlemstep  9334  rebtwn2zlemstep  9339  addmodlteq  9480  mulexpzap  9613  leexp1a  9628  expnbnd  9693  faclbnd  9765  cjap  9931  caucvgre  10005  cvg1nlemres  10009  resqrexlemglsq  10046  resqrexlemga  10047  sqrtsq  10068  ltabs  10111  abs3lem  10135  cau3lem  10138  maxleim  10229  rexico  10245  minmax  10250  climcau  10322  climrecvg1n  10323  sumeq2d  10334  sumeq2  10335  dvdsle  10389  zsupcllemstep  10485  dvdsbnd  10492  gcdsupex  10493  gcdsupcl  10494  bezoutlemmain  10531  bezoutlemzz  10535  bezoutlembi  10538  dfgcd3  10543  dvdsmulgcd  10558  lcmcllem  10593  lcmgcdlem  10603  ncoprmgcdne1b  10615  pw2dvdslemn  10687  oddpwdclemxy  10691
  Copyright terms: Public domain W3C validator