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

Theorem sseliALT 4571
 Description: Alternate proof of sseli 3493 illustrating the use of the weak deduction theorem to prove it from the inference sselii 3494. (Contributed by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
sseliALT.1
Assertion
Ref Expression
sseliALT

Proof of Theorem sseliALT
StepHypRef Expression
1 biidd 237 . 2
2 eleq2 2533 . 2
3 eleq1 2532 . 2
4 sseq1 3518 . . . 4
5 sseq2 3519 . . . 4
6 biidd 237 . . . 4
7 sseq1 3518 . . . 4
8 sseq2 3519 . . . 4
9 biidd 237 . . . 4
10 sseliALT.1 . . . 4
11 ssid 3516 . . . 4
124, 5, 6, 7, 8, 9, 10, 11keephyp3v 3999 . . 3
13 eleq2 2533 . . . 4
14 biidd 237 . . . 4
15 eleq1 2532 . . . 4
16 eleq2 2533 . . . 4
17 biidd 237 . . . 4
18 eleq1 2532 . . . 4
19 0ex 4570 . . . . 5
2019snid 4048 . . . 4
2113, 14, 15, 16, 17, 18, 20elimhyp3v 3993 . . 3
2212, 21sselii 3494 . 2
231, 2, 3, 22dedth3v 3989 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1374   wcel 1762   wss 3469  c0 3778  cif 3932  csn 4020 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-nul 4569 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-v 3108  df-dif 3472  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator