Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Variable E Y R : Prop.
- Theorem Thm06 : ((E -> (Y \/ R)) /\ (Y -> R)) -> (~R -> ~E).
- unfold not.
- I_imp I1.
- I_imp I2.
- I_imp I3.
- E_et I1.
- E_imp I1g.
- Hyp I3.
- E_ou I1gc.
- E_imp I1d.
- Hyp I1gcg.
- E_imp I2.
- Hyp I1dc.
- Hyp I2c.
- E_imp I2.
- Hyp I1gcd.
- Hyp I2c.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
