Theorem or 196

Description: 'Or' elimination, and its converse. Axiom io in iset.mm.

Assertion

Ref	Expression
or	⊦ (((𝜑 ∨ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜒) ∧ (𝜓 → 𝜒)))

Proof of Theorem or

Step	Hyp	Ref	Expression

Syntax hints:   → wim 180   ∧ wand 182   ∨ wor 184   ↔ wbi 188

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)