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  4357  opthprc  5702  imadif  6600  frxp2  8123  xrsupss  13269  mdegleb  25969  difrab2  32427  ind1a  32782  poimirlem30  37644  ifpdfan2  43452  ifpdfan  43455  ifpnot  43459  ifpid2  43460  uneqsn  44014  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb4  48026