![]() |
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 2640 2eu1v 2641 rspcebdv 3602 elpwunsn 4692 trel 5279 preddowncl 6345 predpoirr 6346 predfrirr 6347 funfvima 7247 ordsucss 7827 mapfset 8879 ac10ct 10077 ltaprlem 11087 infrelb 12251 nnmulcl 12288 ico0 13424 ioc0 13425 clwlkclwwlkfo 29942 n4cyclfrgr 30224 chlimi 31167 atcvatlem 32318 rdgssun 37085 eel12131 44389 lidldomn1 47608 |
Copyright terms: Public domain | W3C validator |