![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > axc4i | Structured version Unicode version |
Description: Inference version of axc4 1800. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
axc4i.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
axc4i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 1836 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | axc4i.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | alrimi 1816 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-12 1794 |
This theorem depends on definitions: df-bi 185 df-ex 1588 df-nf 1591 |
This theorem is referenced by: hbae 2015 hbsb2 2059 hbsb2a 2061 hbsb2e 2062 reu6 3255 axunndlem1 8873 axregndOLD 8885 axacndlem3 8890 axacndlem5 8892 axacnd 8893 pm11.57 29810 pm11.59 29812 axc5c4c711toc7 29826 axc11next 29828 hbalg 31616 ax6e2eq 31618 ax6e2eqVD 31995 bj-nfs1t 32562 bj-hbsb2v 32626 bj-hbsb2av 32628 |
Copyright terms: Public domain | W3C validator |