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  6879  finexdc  6880  dcfi  6958  difinfsn  7077  nnnninfeq2  7105  nninfisol  7109  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  suplocexprlemru  7681  suplocsrlemb  7768  suplocsrlem  7770  supinfneg  9554  infsupneg  9555  xaddf  9801  xaddval  9802  nn0ltexp2  10644  hashunlem  10739  xrmaxiflemcl  11208  xrmaxiflemlub  11211  xrmaxltsup  11221  sumeq2  11322  fsumconst  11417  prodeq2  11520  fprodconst  11583  sgrpidmndm  12656  cncnp  13024  neitx  13062  dedekindeulemlu  13393  suplociccreex  13396  dedekindicclemlu  13402  cnplimclemr  13432  limccnp2cntop  13440  logbgcd1irrap  13682  lgsval  13699
  Copyright terms: Public domain W3C validator