Theorem biorfri 938

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

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

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 847

This theorem is referenced by:  pm4.43  1023  dn1  1058  indifdirOLD  4309  un0  4413  opthprc  5763  imadif  6661  frxp2  8181  xrsupss  13367  mdegleb  26115  difrab2  32517  ind1a  33975  poimirlem30  37559  ifpdfan2  43366  ifpdfan  43369  ifpnot  43373  ifpid2  43374  uneqsn  43928  usgrexmpl2nb1  47767  usgrexmpl2nb2  47768  usgrexmpl2nb4  47770