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 199 1 (𝜓 ↔ (𝜓𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ 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 197  df-or 384 This theorem is referenced by:  pm4.43  1006  dn1  1046  indifdir  4026  un0  4110  opthprc  5324  imadif  6134  xrsupss  12352  mdegleb  24043  difrab2  29667  ind1a  30411  poimirlem30  33770  ifpdfan2  38327  ifpdfan  38330  ifpnot  38334  ifpid2  38335  uneqsn  38841
 Copyright terms: Public domain W3C validator