MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biorf Structured version   Visualization version   GIF version

Theorem biorf 936
Description: A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
Assertion
Ref Expression
biorf 𝜑 → (𝜓 ↔ (𝜑𝜓)))

Proof of Theorem biorf
StepHypRef Expression
1 olc 867 . 2 (𝜓 → (𝜑𝜓))
2 orel1 888 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 225 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wo 846
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 206  df-or 847
This theorem is referenced by:  biortn  937  pm5.55  948  pm5.75  1028  3bior1fd  1476  3bior2fd  1478  norasslem3  1538  euor  2612  euorv  2613  euor2  2614  eueq3  3674  unineq  4242  ifor  4545  difprsnss  4764  eqsn  4794  pr1eqbg  4819  disjprgw  5105  disjprg  5106  disjxun  5108  opthwiener  5476  opthprc  5701  frxp2  8081  swoord1  8686  brwdomn0  9512  fpwwe2lem12  10585  ne0gt0  11267  xrinfmss  13236  sumsplit  15660  sadadd2lem2  16337  coprm  16594  vdwlem11  16870  lvecvscan  20588  lvecvscan2  20589  mplcoe1  21454  mplcoe5  21457  maducoeval2  22005  xrsxmet  24188  itg2split  25130  plydiveu  25674  quotcan  25685  coseq1  25897  angrtmuld  26174  leibpilem2  26307  leibpi  26308  wilthlem2  26434  tgldimor  27486  tgcolg  27538  axcontlem7  27961  elntg2  27976  nb3grprlem2  28371  eupth2lem2  29205  eupth2lem3lem6  29219  nmlnogt0  29781  hvmulcan  30056  hvmulcan2  30057  rmounid  31465  disjunsn  31554  xrdifh  31725  bj-biorfi  35077  bj-snmoore  35613  nlpineqsn  35908  wl-ifp-ncond1  35964  itgaddnclem2  36166  biorfd  36717  elpadd0  38301  fsuppind  40794  or3or  42369
  Copyright terms: Public domain W3C validator