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

Theorem bj-biorfi 33470
Description: This should be labeled "biorfi" while the current biorfi 407 should be labelled "biorfri". The dual of biorf 405 is not biantr 929 but iba 503 (and ibar 504). 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  |-  -.  ph
Assertion
Ref Expression
bj-biorfi  |-  ( ps  <->  (
ph  \/  ps )
)

Proof of Theorem bj-biorfi
StepHypRef Expression
1 bj-biorfi.1 . 2  |-  -.  ph
2 biorf 405 . 2  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  (
ph  \/  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  bj-falor  33471
  Copyright terms: Public domain W3C validator