![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61d2 | Structured version Visualization version Unicode version |
Description: Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
Ref | Expression |
---|---|
pm2.61d2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm2.61d2.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.61d2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61d2.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | pm2.61d2.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | pm2.61d 162 |
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 |
This theorem is referenced by: pm2.61ii 169 jaoi 381 nfald2 2167 nfsbd 2273 2ax6elem 2280 sbal1 2291 sbal2 2292 nfabd2 2613 rgen2a 2817 relimasn 5194 nfriotad 6265 tfinds 6691 curry1val 6894 curry2val 6898 onfununi 7065 findcard2s 7817 xpfi 7847 fiint 7853 acndom 8487 dfac12k 8582 iundom2g 8970 nqereu 9359 ltapr 9475 xrmax1 11477 xrmin2 11480 max1ALT 11488 hasheq0 12551 swrdnd2 12796 cshw1 12928 bezout 14522 ptbasfi 20608 filcon 20910 pcopt 22065 ioorinv 22540 ioorinvOLD 22545 itg1addlem2 22667 itg1addlem4 22669 itgss 22781 bddmulibl 22808 wlkdvspthlem 25349 mdsymlem6 28073 sumdmdlem2 28084 bj-ax6elem1 31276 wl-equsb4 31897 wl-sbalnae 31904 poimirlem13 31965 poimirlem25 31977 poimirlem27 31979 sgoldbaltlem1 38890 |
Copyright terms: Public domain | W3C validator |