Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqrdavOLD Structured version   Unicode version

Theorem eqrdavOLD 2440
 Description: Obsolete proof of eqrdav 2439 as of 19-Nov-2019. (Contributed by NM, 7-Nov-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
eqrdav.1
eqrdav.2
eqrdav.3
Assertion
Ref Expression
eqrdavOLD
Distinct variable groups:   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem eqrdavOLD
StepHypRef Expression
1 eqrdav.1 . . . 4
2 eqrdav.3 . . . . . 6
32biimpd 207 . . . . 5
43impancom 440 . . . 4
51, 4mpd 15 . . 3
6 eqrdav.2 . . . 4
72exbiri 622 . . . . . 6
87com23 78 . . . . 5
98imp 429 . . . 4
106, 9mpd 15 . . 3
115, 10impbida 830 . 2
1211eqrdv 2438 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1381   wcel 1802 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-ext 2419 This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2433 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator