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

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
StepHypRef Expression
1 orc 867 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 pm2.53 851 . . 3 ((𝜓𝜑) → (¬ 𝜓𝜑))
42, 3mt3i 151 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 212 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator