ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simp-4r GIF version

Theorem simp-4r 537
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-4r (((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r
StepHypRef Expression
1 simpllr 529 . 2 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
21adantr 274 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-5r  539  fimax2gtri  6875  finexdc  6876  dcfi  6954  difinfsn  7073  nnnninfeq2  7101  nninfisol  7105  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  suplocexprlemru  7668  suplocsrlemb  7755  suplocsrlem  7757  supinfneg  9541  infsupneg  9542  xaddf  9788  xaddval  9789  nn0ltexp2  10631  hashunlem  10726  xrmaxiflemcl  11195  xrmaxiflemlub  11198  xrmaxltsup  11208  sumeq2  11309  fsumconst  11404  prodeq2  11507  fprodconst  11570  sgrpidmndm  12643  cncnp  12983  neitx  13021  dedekindeulemlu  13352  suplociccreex  13355  dedekindicclemlu  13361  cnplimclemr  13391  limccnp2cntop  13399  logbgcd1irrap  13641  lgsval  13658
  Copyright terms: Public domain W3C validator