Theorem ornld

Selecting one statement from a disjunction if one of the disjuncted statements is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

Conclusion

\( \vdash \varphi \rightarrow (\varphi \rightarrow \theta \vee \tau) \wedge \neg \theta \rightarrow \tau \)

Proof

pm3.35

ord _

expimpd _