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

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

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 103 . 2 ((𝜑𝜓) → 𝜓)
21ad2antrr 457 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  f1o2ndf1  5849  tfrlem1  5923  fopwdom  6310  phplem4dom  6324  phpm  6327  phplem4on  6329  fidifsnen  6331  diffisn  6350  diffifi  6351  addcmpblnq  6463  mulcmpblnq  6464  ordpipqqs  6470  ltexnqq  6504  enq0tr  6530  addcmpblnq0  6539  mulcmpblnq0  6540  nnnq0lem1  6542  prssnqu  6576  prarloclemup  6591  nqprl  6647  nqpru  6648  mullocpr  6667  cauappcvgprlemladdfu  6750  cauappcvgprlemladdrl  6753  caucvgprlemm  6764  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlemlim  6777  caucvgprprlemml  6790  caucvgprprlemloc  6799  caucvgprprlemlim  6807  addcmpblnr  6822  mulcmpblnrlemg  6823  mulcmpblnr  6824  ltsrprg  6830  srpospr  6865  caucvgsrlemoffres  6882  axcaucvglemcau  6970  cnegexlem3  7186  negeu  7200  add20  7467  rimul  7574  apreap  7576  cru  7591  apreim  7592  apsym  7595  apcotr  7596  apadd1  7597  apneg  7600  mulext1  7601  apti  7611  mulap0  7633  prodgt0  7816  ltmul12a  7824  ledivdiv  7854  lediv12a  7858  qapne  8572  ixxss12  8773  ioodisj  8859  fznlem  8903  qtri3or  9096  qbtwnzlemstep  9101  rebtwn2zlemstep  9105  mulexpzap  9269  leexp1a  9283  expnbnd  9346  cjap  9480  caucvgre  9554  cvg1nlemres  9558  resqrexlemglsq  9594  resqrexlemga  9595  sqrtsq  9616  ltabs  9657  abs3lem  9681  cau3lem  9684  climcau  9840  climrecvg1n  9841
  Copyright terms: Public domain W3C validator