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