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 52 | . 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: 3imp3i2an 1270 2eu1 2541 elpwunsn 4171 trel 4687 trssOLD 4690 preddowncl 5624 predpoirr 5625 predfrirr 5626 funfvima 6396 ordsucss 6910 ac10ct 8740 ltaprlem 9745 infrelb 10885 nnmulcl 10920 ico0 12092 ioc0 12093 clwlkfoclwwlk 26372 n4cyclfrgra 26545 vdgn0frgrav2 26551 chlimi 27475 atcvatlem 28628 eel12131 37959 clwlksfoclwwlk 41270 n4cyclfrgr 41461 lidldomn1 41711 |
Copyright terms: Public domain | W3C validator |