uzind - Metamath

Theorem uzind

Hypotheses

Ref	Expression
uzind.1	|- (j = M -> (ph <-> ps))
uzind.2	|- (j = k -> (ph <-> ch))
uzind.3	|- (j = (k + 1) -> (ph <-> th))
uzind.4	|- (j = N -> (ph <-> ta))
uzind.5	|- (M e. ZZ -> ps)
uzind.6	|- ((M e. ZZ /\ k e. ZZ /\ M <_ k) -> (ch -> th))

Distinct variable groups:     j,N    j,ps    j,ch    j,th    j,ta    k,ph    j,k,M

Proof

Ref	Expression
pm3.27d	1  show/hide details |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ta)