| 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 3610 rspc2gv 3632 intss1 4963 fvopab3ig 7012 suppimacnv 8199 odi 8617 nndi 8661 preleqALT 9657 inf3lem2 9669 pr2neOLD 10045 zorn2lem7 10542 uzind2 12711 ssfzo12 13798 elfznelfzo 13811 injresinj 13827 suppssfz 14035 sqlecan 14248 fi1uzind 14546 cramerimplem2 22690 fiinopn 22907 uhgr0v0e 29255 0uhgrsubgr 29296 0uhgrrusgr 29596 ewlkprop 29621 umgrwwlks2on 29977 3cyclfrgrrn1 30304 3cyclfrgrrn 30305 vdgn1frgrv2 30315 dvrunz 37961 ee223 44654 afveu 47165 afv2eu 47250 lindslinindsimp2 48380 nn0sumshdiglemB 48541 |
| Copyright terms: Public domain | W3C validator |