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  4347  opthprc  5687  imadif  6570  frxp2  8084  xrsupss  13229  mdegleb  25985  difrab2  32460  ind1a  32815  poimirlem30  37629  ifpdfan2  43436  ifpdfan  43439  ifpnot  43443  ifpid2  43444  uneqsn  43998  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb4  48020