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

Theorem simp-4r 531
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 523 . 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  533  fimax2gtri  6795  finexdc  6796  difinfsn  6985  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  suplocexprlemru  7534  suplocsrlemb  7621  suplocsrlem  7623  supinfneg  9397  infsupneg  9398  xaddf  9634  xaddval  9635  hashunlem  10557  xrmaxiflemcl  11021  xrmaxiflemlub  11024  xrmaxltsup  11034  sumeq2  11135  fsumconst  11230  prodeq2  11333  cncnp  12409  neitx  12447  dedekindeulemlu  12778  suplociccreex  12781  dedekindicclemlu  12787  cnplimclemr  12817  limccnp2cntop  12825
  Copyright terms: Public domain W3C validator