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  1038  dn1  1071  un0  4351  opthprc  5716  imadif  6609  frxp2  8128  ind1a  12220  xrsupss  13326  mdegleb  26182  difrab2  32754  poimirlem30  38161  ifpdfan2  44051  ifpdfan  44054  ifpnot  44058  ifpid2  44059  uneqsn  44613  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb4  48655