Theorem biorfi 939

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 867	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜑))
2		biorfi.1	. . 3 ⊢ ¬ 𝜑
3		pm2.53 851	. . 3 ⊢ ((𝜓 ∨ 𝜑) → (¬ 𝜓 → 𝜑))
4	2, 3	mt3i 151	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜓)
5	1, 4	impbii 212	1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∨ wo 847

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 210  df-or 848

This theorem is referenced by:  pm4.43  1023  dn1  1058  indifdirOLD  4200  un0  4305  opthprc  5613  imadif  6464  xrsupss  12899  mdegleb  24962  difrab2  30564  ind1a  31699  frxp2  33528  poimirlem30  35544  ifpdfan2  40755  ifpdfan  40758  ifpnot  40762  ifpid2  40763  uneqsn  41310