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  4344  opthprc  5715  imadif  6616  frxp2  8145  ind1a  12312  xrsupss  13420  mdegleb  26362  difrab2  33076  poimirlem30  38536  ifpdfan2  44422  ifpdfan  44425  ifpnot  44429  ifpid2  44430  uneqsn  44984  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb4  49077