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 3608 rspc2gv 3629 intss1 4882 fvopab3ig 6757 suppimacnv 7830 odi 8194 nndi 8238 preleqALT 9068 inf3lem2 9080 pr2ne 9419 zorn2lem7 9912 uzind2 12063 ssfzo12 13118 elfznelfzo 13130 injresinj 13146 suppssfz 13350 sqlecan 13559 fi1uzind 13843 cramerimplem2 21221 fiinopn 21437 uhgr0v0e 26947 0uhgrsubgr 26988 0uhgrrusgr 27287 ewlkprop 27312 umgrwwlks2on 27663 3cyclfrgrrn1 27991 3cyclfrgrrn 27992 vdgn1frgrv2 28002 dvrunz 35113 ee223 40845 afveu 43229 afv2eu 43314 lindslinindsimp2 44446 nn0sumshdiglemB 44608 |
Copyright terms: Public domain | W3C validator |