Theorem oplem1

Description: A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995) (Proof shortened by Wolf Lammen, 8-Dec-2012)

	Ref	Expression
Hypotheses	oplem1.1	|- ( ph -> ( ps \/ ch ) )
	oplem1.2	|- ( ph -> ( th \/ ta ) )
	oplem1.3	|- ( ps <-> th )
	oplem1.4	|- ( ch -> ( th <-> ta ) )
Assertion	oplem1	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		oplem1.1	|- ( ph -> ( ps \/ ch ) )
2		oplem1.2	|- ( ph -> ( th \/ ta ) )
3		oplem1.3	|- ( ps <-> th )
4		oplem1.4	|- ( ch -> ( th <-> ta ) )
5	3	notbii	|- ( -. ps <-> -. th )
6	1	ord	|- ( ph -> ( -. ps -> ch ) )
7	5 6	syl5bir	|- ( ph -> ( -. th -> ch ) )
8	2	ord	|- ( ph -> ( -. th -> ta ) )
9	7 8	jcad	|- ( ph -> ( -. th -> ( ch /\ ta ) ) )
10	4	biimpar	|- ( ( ch /\ ta ) -> th )
11	9 10	syl6	|- ( ph -> ( -. th -> th ) )
12	11	pm2.18d	|- ( ph -> th )
13	12 3	sylibr	|- ( ph -> ps )