![]() |
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 3553 rspc2gv 3571 intss1 4797 fvopab3ig 6631 suppimacnv 7692 odi 8055 nndi 8099 preleqALT 8926 inf3lem2 8938 pr2ne 9277 zorn2lem7 9770 uzind2 11924 ssfzo12 12980 elfznelfzo 12992 injresinj 13008 suppssfz 13212 sqlecan 13421 fi1uzind 13701 cramerimplem2 20977 fiinopn 21193 uhgr0v0e 26703 0uhgrsubgr 26744 0uhgrrusgr 27043 ewlkprop 27068 umgrwwlks2on 27423 3cyclfrgrrn1 27756 3cyclfrgrrn 27757 vdgn1frgrv2 27767 dvrunz 34764 ee223 40507 afveu 42868 afv2eu 42953 lindslinindsimp2 43998 nn0sumshdiglemB 44161 |
Copyright terms: Public domain | W3C validator |