Theorem biorfi 938

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

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

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 847

This theorem is referenced by:  pm4.43  1022  dn1  1057  indifdirOLD  4286  un0  4391  opthprc  5741  imadif  6633  frxp2  8130  xrsupss  13288  mdegleb  25582  difrab2  31738  ind1a  33017  poimirlem30  36518  ifpdfan2  42214  ifpdfan  42217  ifpnot  42221  ifpid2  42222  uneqsn  42776