Theorem biorfri 950

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 949	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 881	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 277	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∨ wo 858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-or 859

This theorem is referenced by:  pm4.43  1035  dn1  1068  un0  4347  opthprc  5709  imadif  6601  frxp2  8119  ind1a  12203  xrsupss  13309  mdegleb  26104  difrab2  32645  poimirlem30  38113  ifpdfan2  44003  ifpdfan  44006  ifpnot  44010  ifpid2  44011  uneqsn  44565  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb4  48621