![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.21bi | Structured version Visualization version Unicode version |
Description: Inference form of 19.21 1998 and also deduction form of sp 1948. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
19.21bi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
19.21bi |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.21bi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sp 1948 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-12 1944 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 |
This theorem is referenced by: 19.21bbi 1959 2ax6e 2290 eqeq1dALT 2465 eleq2dALT 2527 r19.21biOLD 2770 elrab3t 3207 ssel 3438 pocl 4781 funmo 5617 funun 5643 fununi 5671 findcard 7836 findcard2 7837 axpowndlem4 9051 axregndlem2 9054 axinfnd 9057 prcdnq 9444 dfrtrcl2 13174 relexpindlem 13175 bnj1379 29691 bnj1052 29833 bnj1118 29842 bnj1154 29857 bnj1280 29878 dftrcl3 36357 dfrtrcl3 36370 vk15.4j 36929 hbimpg 36965 |
Copyright terms: Public domain | W3C validator |