Theorem biorfri 952

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 951	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 883	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 278	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

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

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 861

This theorem is referenced by:  pm4.43  1040  dn1  1073  un0  4352  opthprc  5727  imadif  6622  frxp2  8141  ind1a  12230  xrsupss  13336  mdegleb  26202  difrab2  32822  poimirlem30  38279  ifpdfan2  44169  ifpdfan  44172  ifpnot  44176  ifpid2  44177  uneqsn  44731  usgrexmpl2nb1  48774  usgrexmpl2nb2  48775  usgrexmpl2nb4  48777