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

Theorem biorfi 422
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 400 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 orel2 398 . . 3 𝜑 → ((𝜓𝜑) → 𝜓))
42, 3ax-mp 5 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 199 1 (𝜓 ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383
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 197  df-or 385
This theorem is referenced by:  pm4.43  967  dn1  1007  indifdir  3864  un0  3944  opthprc  5132  imadif  5936  xrsupss  12089  mdegleb  23741  ind1a  29882  poimirlem30  33098  ifpdfan2  37315  ifpdfan  37318  ifpnot  37322  ifpid2  37323  uneqsn  37830
  Copyright terms: Public domain W3C validator