Theorem biorfi 422

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 400	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜑))
2		biorfi.1	. . 3 ⊢ ¬ 𝜑
3		orel2 398	. . 3 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))
4	2, 3	ax-mp 5	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜓)
5	1, 4	impbii 199	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  pm4.43  968  dn1  1008  indifdir  3883  un0  3967  opthprc  5167  imadif  5973  xrsupss  12139  mdegleb  23824  difrab2  29339  ind1a  30081  poimirlem30  33439  ifpdfan2  37807  ifpdfan  37810  ifpnot  37814  ifpid2  37815  uneqsn  38321