Definition eqtypri 71

Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)

Hypotheses

Ref	Expression
eqtypri.1	|- A:al
eqtypri.2	|- R |= [B = A]

Assertion

Ref	Expression
eqtypri	|- B:al

Detailed syntax breakdown of Definition eqtypri

Step	Hyp	Ref	Expression
1		hal	. 2 type al
2		tb	. 2 term B
3	1, 2	wffMMJ2t 12	1 wff B:al

This definition is referenced by:  mpbir  77  3eqtr4i  86  hbc  100  wal  124  wfal  125  wan  126  wim  127  wnot  128  wex  129  wor  130  weu  131