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  4354  opthprc  5730  imadif  6627  frxp2  8149  ind1a  12247  xrsupss  13353  mdegleb  26258  difrab2  32881  poimirlem30  38341  ifpdfan2  44229  ifpdfan  44232  ifpnot  44236  ifpid2  44237  uneqsn  44791  usgrexmpl2nb1  48837  usgrexmpl2nb2  48838  usgrexmpl2nb4  48840