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

Theorem biorfi 953
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 885 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 orel2 906 . . 3 𝜑 → ((𝜓𝜑) → 𝜓))
42, 3ax-mp 5 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 200 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wo 865
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 198  df-or 866
This theorem is referenced by:  pm4.43  1037  dn1  1073  indifdir  4079  un0  4159  opthprc  5361  imadif  6178  xrsupss  12351  mdegleb  24032  difrab2  29658  ind1a  30400  poimirlem30  33746  ifpdfan2  38301  ifpdfan  38304  ifpnot  38308  ifpid2  38309  uneqsn  38815
  Copyright terms: Public domain W3C validator