![]() |
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 44 | 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 55 rspc 3454 rspc2gv 3471 intss1 4626 fvopab3ig 6420 suppimacnv 7457 odi 7813 nndi 7857 preleqALT 8676 inf3lem2 8690 pr2ne 9028 zorn2lem7 9526 uzind2 11672 ssfzo12 12769 elfznelfzo 12781 injresinj 12797 suppssfz 13001 sqlecan 13178 fi1uzind 13481 cramerimplem2 20710 fiinopn 20926 uhgr0v0e 26353 0uhgrsubgr 26394 0uhgrrusgr 26709 ewlkprop 26734 umgrwwlks2on 27105 3cyclfrgrrn1 27467 3cyclfrgrrn 27468 vdgn1frgrv2 27478 dvrunz 34085 ee223 39384 afveu 41753 lindslinindsimp2 42780 nn0sumshdiglemB 42942 |
Copyright terms: Public domain | W3C validator |