Theorem biorfri 940

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

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

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 849

This theorem is referenced by:  pm4.43  1025  dn1  1058  un0  4335  opthprc  5688  imadif  6576  frxp2  8087  ind1a  12161  xrsupss  13252  mdegleb  26039  difrab2  32582  poimirlem30  37985  ifpdfan2  43908  ifpdfan  43911  ifpnot  43915  ifpid2  43916  uneqsn  44470  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb4  48523