### Nuprl Lemma : two-implies-quotient-true

[P,Q,R:ℙ].  ((P   R)  {⇃(P)  ⇃(Q)  ⇃(R)})

Proof

Definitions occuring in Statement :  quotient: x,y:A//B[x; y] uall: [x:A]. B[x] prop: guard: {T} implies:  Q true: True
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] implies:  Q member: t ∈ T prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a quotient: x,y:A//B[x; y] and: P ∧ Q all: x:A. B[x] subtype_rel: A ⊆B true: True
Lemmas referenced :  quotient_wf true_wf equiv_rel_true quotient-member-eq equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation rename introduction pointwiseFunctionalityForEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality hypothesis because_Cache independent_isectElimination pertypeElimination productElimination dependent_functionElimination applyEquality functionEquality independent_functionElimination natural_numberEquality productEquality universeEquality

Latex:
\mforall{}[P,Q,R:\mBbbP{}].    ((P  {}\mRightarrow{}  Q  {}\mRightarrow{}  R)  {}\mRightarrow{}  \{\00D9(P)  {}\mRightarrow{}  \00D9(Q)  {}\mRightarrow{}  \00D9(R)\})

Date html generated: 2016_05_14-AM-06_08_51
Last ObjectModification: 2015_12_26-AM-11_48_23

Theory : quot_1

Home Index