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  4401  opthprc  5754  imadif  6655  frxp2  8174  xrsupss  13354  mdegleb  26126  difrab2  32539  ind1a  34013  poimirlem30  37649  ifpdfan2  43467  ifpdfan  43470  ifpnot  43474  ifpid2  43475  uneqsn  44029  usgrexmpl2nb1  47940  usgrexmpl2nb2  47941  usgrexmpl2nb4  47943