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

Theorem biorf 934
 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 865 . 2 (𝜓 → (𝜑𝜓))
2 orel1 886 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 229 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  biortn  935  pm5.55  946  pm5.75  1026  3bior1fd  1472  3bior2fd  1474  norasslem3  1533  euor  2696  euorv  2697  euor2  2698  eueq3  3677  unineq  4228  ifor  4491  difprsnss  4705  eqsn  4735  pr1eqbg  4760  disjprgw  5037  disjprg  5038  disjxun  5040  opthwiener  5381  opthprc  5593  swoord1  8307  brwdomn0  9021  fpwwe2lem13  10053  ne0gt0  10734  xrinfmss  12691  sumsplit  15114  sadadd2lem2  15788  coprm  16044  vdwlem11  16316  lvecvscan  19874  lvecvscan2  19875  mplcoe1  20703  mplcoe5  20706  maducoeval2  21243  xrsxmet  23412  itg2split  24351  plydiveu  24892  quotcan  24903  coseq1  25115  angrtmuld  25392  leibpilem2  25525  leibpi  25526  wilthlem2  25652  tgldimor  26294  tgcolg  26346  axcontlem7  26762  elntg2  26777  nb3grprlem2  27169  eupth2lem2  28002  eupth2lem3lem6  28016  nmlnogt0  28578  hvmulcan  28853  hvmulcan2  28854  rmounid  30264  disjunsn  30352  xrdifh  30513  bj-biorfi  33991  bj-snmoore  34489  nlpineqsn  34786  itgaddnclem2  35074  elpadd0  37063  fsuppind  39403  or3or  40657
 Copyright terms: Public domain W3C validator