Destructive_Dilemma_Formulation_1_v2
Provedproofwikiretry
Destructive dilemma: if p->q and r->s, then (not q or not s) implies (not p or not r).
Formal statement
theorem Destructive_Dilemma_Formulation_1_v2 (p q r s : Prop) (hpq : p → q) (hrs : r → s) : (¬q ∨ ¬s) → (¬p ∨ ¬r) := by sorry