Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax6 | Structured version Visualization version Unicode version |
Description: Theorem showing that ax-6 1888
follows from the weaker version ax6v 1889.
(Even though this theorem depends on ax-6 1888,
all references of ax-6 1888 are
made via ax6v 1889. An earlier version stated ax6v 1889
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1888 so that all proofs can be traced back to ax6v 1889. When possible, use the weaker ax6v 1889 rather than ax6 2251 since the ax6v 1889 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) |
Ref | Expression |
---|---|
ax6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax6e 2250 | . 2 | |
2 | df-ex 1705 | . 2 | |
3 | 1, 2 | mpbi 220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 |
This theorem is referenced by: axc10 2252 |
Copyright terms: Public domain | W3C validator |