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  4348  opthprc  5696  imadif  6584  frxp2  8096  xrsupss  13236  mdegleb  26037  difrab2  32583  ind1a  32948  poimirlem30  37895  ifpdfan2  43813  ifpdfan  43816  ifpnot  43820  ifpid2  43821  uneqsn  44375  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb4  48389