Theorem biorfi 933

Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.)

Hypothesis

Ref	Expression
biorfi.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
biorfi	⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Proof of Theorem biorfi

Step	Hyp	Ref	Expression
1		orc 862	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜑))
2		biorfi.1	. . 3 ⊢ ¬ 𝜑
3		pm2.53 846	. . 3 ⊢ ((𝜓 ∨ 𝜑) → (¬ 𝜓 → 𝜑))
4	2, 3	mt3i 151	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜓)
5	1, 4	impbii 210	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∨ wo 842

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 208  df-or 843

This theorem is referenced by:  pm4.43  1017  dn1  1050  indifdir  4186  un0  4270  opthprc  5509  imadif  6315  xrsupss  12556  mdegleb  24345  difrab2  29949  ind1a  30891  poimirlem30  34474  ifpdfan2  39334  ifpdfan  39337  ifpnot  39341  ifpid2  39342  uneqsn  39879