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

Theorem biorfi 924
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 856 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 orel2 877 . . 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 836
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 837
This theorem is referenced by:  pm4.43  1008  dn1  1044  indifdir  4032  un0  4112  opthprc  5306  imadif  6112  xrsupss  12343  mdegleb  24043  difrab2  29676  ind1a  30420  poimirlem30  33771  ifpdfan2  38333  ifpdfan  38336  ifpnot  38340  ifpid2  38341  uneqsn  38847
  Copyright terms: Public domain W3C validator