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

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
StepHypRef Expression
1 orc 865 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 pm2.53 849 . . 3 ((𝜓𝜑) → (¬ 𝜓𝜑))
42, 3mt3i 149 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 208 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
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  4245  un0  4350  opthprc  5696  imadif  6585  frxp2  8075  xrsupss  13227  mdegleb  25427  difrab2  31424  ind1a  32609  poimirlem30  36099  ifpdfan2  41717  ifpdfan  41720  ifpnot  41724  ifpid2  41725  uneqsn  42279
  Copyright terms: Public domain W3C validator