Nuprl - Pf formula_imp_right

PrintForm Definitions elimination Sections ClassicalProps(jlc) Doc

1. hyp: Formula List
2. M: Formula List
3. N: Formula List
4. q: Formula
5. r: Formula
6. a:Full( < q.hyp,r.(M @ N) > ). a |= < q.hyp,r.(M @ N) >
7. a: Full( < hyp,M @ (qr.N) > )

a |= < hyp,M @ (qr.N) >

By: With a (Analyze -2)

Generated subgoals:

1 6. a: Full( < hyp,M @ (qr.N) > )
a Full( < q.hyp,r.(M @ N) > )

2 6. a: Full( < hyp,M @ (qr.N) > )
7. a |= < q.hyp,r.(M @ N) >
a |= < hyp,M @ (qr.N) >

About:

1	6. `a:` `Full( < hyp,M @ (qr.N) > )` `a Full( < q.hyp,r.(M @ N) > )`
2	6. `a:` `Full( < hyp,M @ (qr.N) > )` 7. `a \|= < q.hyp,r.(M @ N) >` `a \|= < hyp,M @ (qr.N) >`