| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Theorem showing that ax-16 1252 is redundant if ax-17 1012 is included in the
axiom system. The important part of the proof is provided by aev 1250.
See ax16ALT 1313 for an alternate proof that does not require ax-10 1007 or ax-12 1009. This theorem should not be referenced in any proof. Instead, use ax-16 1252 below so that theorems needing ax-16 1252 can be more easily identified. |
| Ref | Expression |
|---|---|
| ax16 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aev 1250 |
. 2
| |
| 2 | ax-17 1012 |
. . . 4
| |
| 3 | sbequ12 1223 |
. . . . 5
| |
| 4 | 3 | biimpcd 162 |
. . . 4
|
| 5 | 2, 4 | 19.20d 1037 |
. . 3
|
| 6 | 2 | hbsb3 1248 |
. . . 4
|
| 7 | stdpc7 1222 |
. . . 4
| |
| 8 | 6, 2, 7 | cbv3 1206 |
. . 3
|
| 9 | 5, 8 | syl6com 53 |
. 2
|
| 10 | 1, 9 | syl 10 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-10 1007 ax-11 1008 ax-12 1009 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 |
| This theorem depends on definitions: df-bi 154 df-an 232 df-ex 1022 df-sb 1214 |