Description: Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994)
Ref | Expression | ||
---|---|---|---|
Hypothesis | simpli.1 | $${\u22a2}\left({\phi}\wedge {\psi}\right)$$ | |
Assertion | simpli | $${\u22a2}{\phi}$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpli.1 | $${\u22a2}\left({\phi}\wedge {\psi}\right)$$ | |
2 | simpl | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\phi}$$ | |
3 | 1 2 | ax-mp | $${\u22a2}{\phi}$$ |