Theorem olc 399

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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜑))
2	1	orrd 393	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  pm1.4  401  pm2.07  411  pm2.46  413  biorf  420  pm1.5  544  pm2.41  596  jaob  821  pm3.48  877  norbi  903  andi  910  pm4.72  919  consensus  998  dedlemb  1002  anifp  1019  cad1  1552  nfntht  1716  nfntht2  1717  19.33  1809  19.33b  1810  dfsb2  2372  mooran2  2527  undif3OLD  3871  undif4  4013  ordelinelOLD  5795  ordssun  5796  tpres  6431  frxp  7247  omopth2  7624  swoord1  7733  swoord2  7734  rankxplim3  8704  fpwwe2lem12  9423  ltapr  9827  zmulcl  11386  nn0lt2  11400  elnn1uz2  11725  mnflt  11917  mnfltpnf  11920  fzm1  12377  expeq0  12846  nn0o1gt2  15040  prm23lt5  15462  vdwlem9  15636  cshwshashlem1  15745  cshwshash  15754  funcres2c  16501  tsrlemax  17160  odlem1  17894  gexlem1  17934  0top  20727  cmpfi  21151  alexsubALTlem3  21793  dyadmbl  23308  plydivex  23990  scvxcvx  24646  gausslemma2dlem0f  25020  nb3grprlem1  26203  1to3vfriswmgr  27042  frgrregorufr  27082  frgrregord13  27142  disjunsn  29293  dfon2lem4  31445  sltsgn1  31568  sltsgn2  31569  dfrdg4  31753  broutsideof2  31924  lineunray  31949  fwddifnp1  31967  meran1  32105  bj-orim2  32236  bj-currypeirce  32239  bj-peircecurry  32240  bj-falor2  32265  bj-sbsb  32520  bj-unrab  32622  wl-orel12  32965  tsor3  33627  paddclN  34647  lcfl6  36308  ifpid3g  37357  ifpim4  37363  rp-fakeanorass  37378  iunrelexp0  37514  clsk1indlem3  37862  19.33-2  38102  ax6e2ndeq  38296  undif3VD  38640  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  disjxp1  38760  stoweidlem26  39580  stoweidlem37  39591  fourierswlem  39784  fouriersw  39785  elaa2lem  39787  salexct  39889  sge0z  39929  sfprmdvdsmersenne  40849  nn0o1gt2ALTV  40934  stgoldbwt  40989  nrhmzr  41191