Theorem biorfi 935

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 863	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜑))
2		biorfi.1	. . 3 ⊢ ¬ 𝜑
3		pm2.53 847	. . 3 ⊢ ((𝜓 ∨ 𝜑) → (¬ 𝜓 → 𝜑))
4	2, 3	mt3i 149	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜓)
5	1, 4	impbii 208	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  pm4.43  1019  dn1  1054  indifdirOLD  4224  un0  4329  opthprc  5650  imadif  6514  xrsupss  13025  mdegleb  25210  difrab2  30824  ind1a  31966  frxp2  33770  poimirlem30  35786  ifpdfan2  41032  ifpdfan  41035  ifpnot  41039  ifpid2  41040  uneqsn  41586