Theorem biorfri 939

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 938	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 870	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 275	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  pm4.43  1024  dn1  1057  un0  4374  opthprc  5723  imadif  6625  frxp2  8148  xrsupss  13330  mdegleb  26026  difrab2  32484  ind1a  32841  poimirlem30  37679  ifpdfan2  43462  ifpdfan  43465  ifpnot  43469  ifpid2  43470  uneqsn  44024  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb4  48019