Theorem pm2.61da2ne 2882

Description: Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)

Hypotheses

Ref	Expression
pm2.61da2ne.1	|- ( ( ph /\ A = B ) -> ps )
pm2.61da2ne.2	|- ( ( ph /\ C = D ) -> ps )
pm2.61da2ne.3	|- ( ( ph /\ ( A =/= B /\ C =/= D ) ) -> ps )

Assertion

Ref	Expression
pm2.61da2ne	|- ( ph -> ps )

Proof of Theorem pm2.61da2ne

Step	Hyp	Ref	Expression
1		pm2.61da2ne.1	. 2 |- ( ( ph /\ A = B ) -> ps )
2		pm2.61da2ne.2	. . . 4 |- ( ( ph /\ C = D ) -> ps )
3	2	adantlr 751	. . 3 |- ( ( ( ph /\ A =/= B ) /\ C = D ) -> ps )
4		pm2.61da2ne.3	. . . 4 |- ( ( ph /\ ( A =/= B /\ C =/= D ) ) -> ps )
5	4	anassrs 680	. . 3 |- ( ( ( ph /\ A =/= B ) /\ C =/= D ) -> ps )
6	3, 5	pm2.61dane 2881	. 2 |- ( ( ph /\ A =/= B ) -> ps )
7	1, 6	pm2.61dane 2881	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-ne 2795

This theorem is referenced by:  pm2.61da3ne  2883  isabvd  18820  xrsxmet  22612  chordthmlem3  24561  mumul  24907  lgsdirnn0  25069  lgsdinn0  25070  lfl1dim  34408  lfl1dim2N  34409  pmodlem2  35133  cdlemg29  35993  cdlemg39  36004  cdlemg44b  36020  dia2dimlem9  36361  dihprrn  36715  dvh3dim  36735  lcfl9a  36794  lclkrlem2l  36807  lcfrlem42  36873  mapdh6kN  37035  hdmap1l6k  37110