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

Theorem biorfi 409
Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.)
Hypothesis
Ref Expression
biorfi.1  |-  -.  ph
Assertion
Ref Expression
biorfi  |-  ( ps  <->  ( ps  \/  ph )
)

Proof of Theorem biorfi
StepHypRef Expression
1 biorfi.1 . 2  |-  -.  ph
2 orc 387 . . 3  |-  ( ps 
->  ( ps  \/  ph ) )
3 orel2 385 . . 3  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
42, 3impbid2 208 . 2  |-  ( -. 
ph  ->  ( ps  <->  ( ps  \/  ph ) ) )
51, 4ax-mp 5 1  |-  ( ps  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  pm4.43  936  dn1  975  stoic1aOLD  1653  indifdir  3730  un0  3788  opthprc  4899  imadif  5674  xrsupss  11596  mdegleb  23005  ind1a  28844  poimirlem30  31928  ifpdfan2  36070  ifpdfan  36073  ifpnot  36077  ifpid2  36078
  Copyright terms: Public domain W3C validator