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  4347  opthprc  5719  imadif  6646  frxp2  8188  ind1a  12358  xrsupss  13466  mdegleb  26412  difrab2  33166  poimirlem30  38760  ifpdfan2  44656  ifpdfan  44659  ifpnot  44663  ifpid2  44664  uneqsn  45217  usgrexmpl2nb1  49335  usgrexmpl2nb2  49336  usgrexmpl2nb4  49338  elif0  50127