### Nuprl Lemma : decidable__and2

`∀[P:ℙ]. ∀[Q:⋂:P. ℙ].  (Dec(P) `` (P `` Dec(Q)) `` Dec(P ∧ Q))`

Proof

Definitions occuring in Statement :  decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` and: `P ∧ Q` isect: `⋂x:A. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` member: `t ∈ T` subtype_rel: `A ⊆r B` prop: `ℙ` guard: `{T}` not: `¬A` and: `P ∧ Q` false: `False`
Lemmas referenced :  decidable_wf not_wf decidable__and
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution unionElimination thin independent_functionElimination hypothesis cut lemma_by_obid isectElimination hypothesisEquality applyEquality lambdaEquality rename equalityTransitivity equalitySymmetry because_Cache sqequalRule inlFormation inrFormation productElimination voidElimination productEquality cumulativity functionEquality isectEquality universeEquality

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}[Q:\mcap{}:P.  \mBbbP{}].    (Dec(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  Dec(Q))  {}\mRightarrow{}  Dec(P  \mwedge{}  Q))

Date html generated: 2016_05_13-PM-03_09_02
Last ObjectModification: 2016_01_06-PM-05_27_22

Theory : core_2

Home Index