Nuprl Lemma : ringeq_int_terms_transitivity

[r:Rng]. ∀[t1,t2,t3:int_term()].  (t1 ≡ t3) supposing (t2 ≡ t3 and t1 ≡ t2)


Definitions occuring in Statement :  ringeq_int_terms: t1 ≡ t2 rng: Rng int_term: int_term() uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  implies:  Q rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q guard: {T} subtype_rel: A ⊆B true: True rng: Rng prop: squash: T all: x:A. B[x] ringeq_int_terms: t1 ≡ t2 uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_wf int_term_wf ringeq_int_terms_wf iff_weakening_equal ring_term_value_wf rng_car_wf true_wf squash_wf equal_wf
Rules used in proof :  isect_memberEquality intEquality functionEquality axiomEquality independent_functionElimination productElimination independent_isectElimination baseClosed imageMemberEquality sqequalRule natural_numberEquality because_Cache functionExtensionality dependent_functionElimination rename setElimination universeEquality equalitySymmetry hypothesis equalityTransitivity hypothesisEquality isectElimination extract_by_obid imageElimination lambdaEquality thin applyEquality lambdaFormation sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

\mforall{}[r:Rng].  \mforall{}[t1,t2,t3:int\_term()].    (t1  \mequiv{}  t3)  supposing  (t2  \mequiv{}  t3  and  t1  \mequiv{}  t2)

Date html generated: 2018_05_21-PM-03_16_01
Last ObjectModification: 2018_01_25-PM-02_18_31

Theory : rings_1

Home Index