Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  biorfi Structured version   Visualization version   GIF version

Theorem biorfi 936
 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
StepHypRef Expression
1 orc 864 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 pm2.53 848 . . 3 ((𝜓𝜑) → (¬ 𝜓𝜑))
42, 3mt3i 151 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 212 1 (𝜓 ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∨ wo 844 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 845 This theorem is referenced by:  pm4.43  1020  dn1  1053  indifdir  4210  un0  4298  opthprc  5581  imadif  6409  xrsupss  12693  mdegleb  24675  difrab2  30278  ind1a  31403  poimirlem30  35106  ifpdfan2  40214  ifpdfan  40217  ifpnot  40221  ifpid2  40222  uneqsn  40769
 Copyright terms: Public domain W3C validator