Theorem biorfi 937

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

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

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 846

This theorem is referenced by:  pm4.43  1021  dn1  1056  indifdirOLD  4250  un0  4355  opthprc  5701  imadif  6590  frxp2  8081  xrsupss  13238  mdegleb  25466  difrab2  31490  ind1a  32707  poimirlem30  36181  ifpdfan2  41857  ifpdfan  41860  ifpnot  41864  ifpid2  41865  uneqsn  42419