Theorem biorfi 421

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

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

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 384

This theorem is referenced by:  pm4.43  1006  dn1  1046  indifdir  4026  un0  4110  opthprc  5324  imadif  6134  xrsupss  12352  mdegleb  24043  difrab2  29667  ind1a  30411  poimirlem30  33770  ifpdfan2  38327  ifpdfan  38330  ifpnot  38334  ifpid2  38335  uneqsn  38841