![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.43d | Structured version Visualization version GIF version |
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43d.1 | ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
pm2.43d | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | pm2.43d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) | |
3 | 1, 2 | mpdi 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: loolin 110 rspct 3442 po2nr 5200 somo 5221 ordelord 5906 tz7.7 5910 funssres 6091 2elresin 6163 dffv2 6434 f1imass 6685 onint 7161 wfrlem12 7596 wfrlem14 7598 onfununi 7608 smoel 7627 tfrlem11 7654 tfr3 7665 omass 7831 nnmass 7875 sbthlem1 8237 php 8311 inf3lem2 8701 cardne 9001 dfac2b 9163 dfac2OLD 9165 indpi 9941 genpcd 10040 ltexprlem7 10076 addcanpr 10080 reclem4pr 10084 suplem2pr 10087 sup2 11191 nnunb 11500 uzwo 11964 xrub 12355 grpid 17678 lsmcss 20258 uniopn 20924 fclsss1 22047 fclsss2 22048 grpoid 27704 spansncvi 28841 pjnormssi 29357 sumdmdlem2 29608 trpredrec 32064 sltval2 32136 meran1 32737 poimirlem31 33771 heicant 33775 hlhilhillem 37772 ee223 39379 eel2122old 39463 afv0nbfvbi 41755 fmtnoprmfac1lem 42004 |
Copyright terms: Public domain | W3C validator |