Theorem biorfri 953

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.43  1040  dn1  1073  un0  4343  opthprc  5714  imadif  6624  frxp2  8163  ind1a  12334  xrsupss  13442  mdegleb  26387  difrab2  33141  poimirlem30  38661  ifpdfan2  44557  ifpdfan  44560  ifpnot  44564  ifpid2  44565  uneqsn  45118  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb4  49226  elif0  50015