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

Theorem biorfi 421
 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 399 . 2 (𝜓 → (𝜓𝜑))
2 biorfi.1 . . 3 ¬ 𝜑
3 orel2 397 . . 3 𝜑 → ((𝜓𝜑) → 𝜓))
42, 3ax-mp 5 . 2 ((𝜓𝜑) → 𝜓)
51, 4impbii 198 1 (𝜓 ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382 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 196  df-or 384 This theorem is referenced by:  pm4.43  964  dn1  1000  indifdir  3842  un0  3919  opthprc  5089  imadif  5887  xrsupss  12011  mdegleb  23628  ind1a  29410  poimirlem30  32609  ifpdfan2  36826  ifpdfan  36829  ifpnot  36833  ifpid2  36834  uneqsn  37341
 Copyright terms: Public domain W3C validator