Theorem bj-falor2

Description: Dual of truan . (Contributed by BJ, 26-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-falor2	$$⊢\left(\perp \vee \phi \right)\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		falim	$$⊢\perp \to \phi$$
2	1	bj-jaoi1	$$⊢\left(\perp \vee \phi \right)\to \phi$$
3		olc	$$⊢\phi \to \left(\perp \vee \phi \right)$$
4	2 3	impbii	$$⊢\left(\perp \vee \phi \right)\leftrightarrow \phi$$