Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm2.43a | Structured version Visualization version GIF version |
Description: Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43a.1 | ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
pm2.43a | ⊢ (𝜓 → (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | pm2.43a.1 | . 2 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒))) | |
3 | 1, 2 | mpid 43 | 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: pm2.43b 53 rspc 3276 intss1 4427 fvopab3ig 6188 suppimacnv 7193 odi 7546 nndi 7590 inf3lem2 8409 pr2ne 8711 zorn2lem7 9207 uzind2 11346 ssfzo12 12427 elfznelfzo 12439 injresinj 12451 suppssfz 12656 sqlecan 12833 fi1uzind 13134 fi1uzindOLD 13140 cramerimplem2 20309 fiinopn 20531 usgraedg4 25916 wlkdvspthlem 26137 usgrcyclnl1 26168 3cyclfrgrarn1 26539 vdn0frgrav2 26550 vdn1frgrav2 26552 vdgn1frgrav2 26553 numclwlk1lem2foa 26618 dvrunz 32923 ee223 37880 afveu 39882 uhgr0v0e 40464 0uhgrsubgr 40503 0uhgrrusgr 40778 ewlkprop 40805 umgrwwlks2on 41161 3cyclfrgrrn1 41455 3cyclfrgrrn 41456 vdgn1frgrv2 41466 av-numclwlk1lem2foa 41521 lindslinindsimp2 42046 nn0sumshdiglemB 42212 |
Copyright terms: Public domain | W3C validator |