Theorem biorfri 938

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 937	. 2 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
3		orcom 869	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
4	2, 3	bitri 275	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  pm4.43  1023  dn1  1058  un0  4417  opthprc  5764  imadif  6662  frxp2  8185  xrsupss  13371  mdegleb  26123  difrab2  32526  ind1a  33983  poimirlem30  37610  ifpdfan2  43425  ifpdfan  43428  ifpnot  43432  ifpid2  43433  uneqsn  43987  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb4  47850