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  4334  opthprc  5695  imadif  6582  frxp2  8094  ind1a  12170  xrsupss  13261  mdegleb  26029  difrab2  32567  poimirlem30  37971  ifpdfan2  43890  ifpdfan  43893  ifpnot  43897  ifpid2  43898  uneqsn  44452  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb4  48511