NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  olc GIF version

Theorem olc 373
Description: Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
olc (φ → (ψ φ))

Proof of Theorem olc
StepHypRef Expression
1 ax-1 5 . 2 (φ → (¬ ψφ))
21orrd 367 1 (φ → (ψ φ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wo 357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
This theorem is referenced by:  pm1.4  375  pm2.07  385  pm2.46  387  biorf  394  pm1.5  508  pm2.41  556  jaob  758  pm3.48  806  andi  837  pm4.72  846  dedlemb  921  consensus  925  cad1  1398  19.33  1607  19.33b  1608  dfsb2  2055  mooran2  2259  euor2  2272  undif3  3515  undif4  3607  phiall  4618  leconnnc  6218  ncslesuc  6266
  Copyright terms: Public domain W3C validator