Theorem bj-biorfi 34765

Description: This should be labeled "biorfi" while the current biorfi 936 should be labeled "biorfri". The dual of biorf 934 is not biantr 803 but iba 528 (and ibar 529). 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 934	. 2 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  bj-falor  34766