Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-biorfi Structured version   Visualization version   GIF version

Theorem bj-biorfi 32905
Description: This should be labeled "biorfi" while the current biorfi 910 should be labeled "biorfri". The dual of biorf 908 is not biantr 1009 but iba 511 (and ibar 512). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
bj-biorfi.1 ¬ 𝜑
Assertion
Ref Expression
bj-biorfi (𝜓 ↔ (𝜑𝜓))

Proof of Theorem bj-biorfi
StepHypRef Expression
1 bj-biorfi.1 . 2 ¬ 𝜑
2 biorf 908 . 2 𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 826
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 827
This theorem is referenced by:  bj-falor  32906
  Copyright terms: Public domain W3C validator