Nuprl Lemma : curry-lemma

A,B,C:ℙ.  (((A ∧ B)  C)    C)


Proof




Definitions occuring in Statement :  prop: all: x:A. B[x] implies:  Q and: P ∧ Q
Definitions unfolded in proof :  prop: member: t ∈ T cand: c∧ B and: P ∧ Q implies:  Q all: x:A. B[x]
Rules used in proof :  universeEquality cumulativity productEquality functionEquality hypothesisEquality independent_pairFormation thin independent_functionElimination sqequalHypSubstitution hypothesis cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}A,B,C:\mBbbP{}.    (((A  \mwedge{}  B)  {}\mRightarrow{}  C)  {}\mRightarrow{}  A  {}\mRightarrow{}  B  {}\mRightarrow{}  C)



Date html generated: 2016_10_21-AM-09_35_22
Last ObjectModification: 2016_09_23-PM-04_31_02

Theory : core_2


Home Index