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 31741
 Description: This should be labeled "biorfi" while the current biorfi 421 should be labeled "biorfri". The dual of biorf 419 is not biantr 968 but iba 523 (and ibar 524). 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 419 . 2 𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ 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:  bj-falor  31742
 Copyright terms: Public domain W3C validator