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  4225  un0  4330  opthprc  5662  imadif  6547  xrsupss  13093  mdegleb  25278  difrab2  30894  ind1a  32036  frxp2  33840  poimirlem30  35855  ifpdfan2  41283  ifpdfan  41286  ifpnot  41290  ifpid2  41291  uneqsn  41846
  Copyright terms: Public domain W3C validator