Theorem biorfri 945

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 944	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 876	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 276	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm4.43  1030  dn1  1063  un0  4329  opthprc  5689  imadif  6576  frxp2  8091  ind1a  12168  xrsupss  13259  mdegleb  26054  difrab2  32592  poimirlem30  38024  ifpdfan2  43914  ifpdfan  43917  ifpnot  43921  ifpid2  43922  uneqsn  44476  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb4  48533