![]() |
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 3600 rspc2gv 3620 intss1 4966 fvopab3ig 6990 suppimacnv 8154 odi 8575 nndi 8619 preleqALT 9608 inf3lem2 9620 pr2neOLD 9996 zorn2lem7 10493 uzind2 12651 ssfzo12 13721 elfznelfzo 13733 injresinj 13749 suppssfz 13955 sqlecan 14169 fi1uzind 14454 cramerimplem2 22168 fiinopn 22385 uhgr0v0e 28475 0uhgrsubgr 28516 0uhgrrusgr 28815 ewlkprop 28840 umgrwwlks2on 29191 3cyclfrgrrn1 29518 3cyclfrgrrn 29519 vdgn1frgrv2 29529 dvrunz 36760 ee223 43328 afveu 45796 afv2eu 45881 lindslinindsimp2 47046 nn0sumshdiglemB 47208 |
Copyright terms: Public domain | W3C validator |