| 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 111 rspct 3608 po2nr 5606 somo 5631 ordelord 6406 tz7.7 6410 funssres 6610 2elresin 6689 dffv2 7004 f1imass 7284 onint 7810 wfrlem12OLD 8360 wfrlem14OLD 8362 onfununi 8381 smoel 8400 tfrlem11 8428 tfr3 8439 omass 8618 nnmass 8662 sbthlem1 9123 pssnn 9208 php 9247 phpOLD 9259 inf3lem2 9669 cardne 10005 dfac2b 10171 indpi 10947 genpcd 11046 ltexprlem7 11082 addcanpr 11086 reclem4pr 11090 suplem2pr 11093 sup2 12224 nnunb 12522 uzwo 12953 xrub 13354 grpid 18993 lsmcss 21710 uniopn 22903 fclsss1 24030 fclsss2 24031 sltval2 27701 grpoid 30539 spansncvi 31671 pjnormssi 32187 sumdmdlem2 32438 acycgrcycl 35152 meran1 36412 bj-animbi 36560 currysetlem2 36949 bj-elsn0 37156 poimirlem31 37658 heicant 37662 hlhilhillem 41966 sn-sup2 42501 ee223 44654 eel2122old 44738 afv0nbfvbi 47163 fmtnoprmfac1lem 47551 |
| Copyright terms: Public domain | W3C validator |