| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pm2.43b | Structured version Visualization version GIF version | ||
| Description: Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.) |
| Ref | Expression |
|---|---|
| pm2.43b.1 | ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒))) |
| Ref | Expression |
|---|---|
| pm2.43b | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.43b.1 | . . 3 ⊢ (𝜓 → (𝜑 → (𝜓 → 𝜒))) | |
| 2 | 1 | pm2.43a 54 | . 2 ⊢ (𝜓 → (𝜑 → 𝜒)) |
| 3 | 2 | com12 32 | 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: 2eu1 2651 2eu1v 2652 rspcebdv 3616 elpwunsn 4684 trel 5268 preddowncl 6353 predpoirr 6354 predfrirr 6355 funfvima 7250 ordsucss 7838 mapfset 8890 ac10ct 10074 ltaprlem 11084 infrelb 12253 nnmulcl 12290 ico0 13433 ioc0 13434 clwlkclwwlkfo 30028 n4cyclfrgr 30310 chlimi 31253 atcvatlem 32404 rdgssun 37379 eel12131 44733 lidldomn1 48147 |
| Copyright terms: Public domain | W3C validator |