Theorem biorfri 946

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

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

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 855

This theorem is referenced by:  pm4.43  1031  dn1  1064  un0  4324  opthprc  5684  imadif  6572  frxp2  8086  ind1a  12165  xrsupss  13256  mdegleb  26050  difrab2  32587  poimirlem30  38030  ifpdfan2  43920  ifpdfan  43923  ifpnot  43927  ifpid2  43928  uneqsn  44482  usgrexmpl2nb1  48535  usgrexmpl2nb2  48536  usgrexmpl2nb4  48538