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  5723  imadif  6621  frxp2  8146  ind1a  12257  xrsupss  13365  mdegleb  26296  difrab2  32981  poimirlem30  38407  ifpdfan2  44311  ifpdfan  44314  ifpnot  44318  ifpid2  44319  uneqsn  44873  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb4  48959