Theorem bj-biorfi 34451

Description: This should be labeled "biorfi" while the current biorfi 939 should be labeled "biorfri". The dual of biorf 937 is not biantr 806 but iba 531 (and ibar 532). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
bj-biorfi.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
bj-biorfi	⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))

Proof of Theorem bj-biorfi

Step	Hyp	Ref	Expression
1		bj-biorfi.1	. 2 ⊢ ¬ 𝜑
2		biorf 937	. 2 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∨ wo 847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-or 848

This theorem is referenced by:  bj-falor  34452