Theorem biorfri 939

Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) (Proof shortened by AV, 10-Aug-2025.)

Hypothesis

Ref	Expression
biorfi.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
biorfri	⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Proof of Theorem biorfri

Step	Hyp	Ref	Expression
1		biorfi.1	. . 3 ⊢ ¬ 𝜑
2	1	biorfi 938	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 870	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 275	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∨ 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 207  df-or 848

This theorem is referenced by:  pm4.43  1024  dn1  1057  un0  4374  opthprc  5729  imadif  6630  frxp2  8151  xrsupss  13333  mdegleb  26039  difrab2  32445  ind1a  32784  poimirlem30  37616  ifpdfan2  43438  ifpdfan  43441  ifpnot  43445  ifpid2  43446  uneqsn  44000  usgrexmpl2nb1  47949  usgrexmpl2nb2  47950  usgrexmpl2nb4  47952