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

Theorem cbvabOLD 2571
 Description: Obsolete proof of cbvab 2570 as of 16-Nov-2019. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
cbvab.1
cbvab.2
cbvab.3
Assertion
Ref Expression
cbvabOLD

Proof of Theorem cbvabOLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cbvab.2 . . . . 5
21nfsb 2236 . . . 4
3 cbvab.1 . . . . . 6
4 cbvab.3 . . . . . . . 8
54equcoms 1847 . . . . . . 7
65bicomd 204 . . . . . 6
73, 6sbie 2203 . . . . 5
8 sbequ 2171 . . . . 5
97, 8syl5bbr 262 . . . 4
102, 9sbie 2203 . . 3
11 df-clab 2415 . . 3
12 df-clab 2415 . . 3
1310, 11, 123bitr4i 280 . 2
1413eqriv 2425 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wceq 1437  wnf 1663  wsb 1789   wcel 1870  cab 2414 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator