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  597  jaob  822  pm3.48  878  norbi  904  andi  911  pm4.72  920  consensus  999  dedlemb  1003  anifp  1020  cad1  1555  nfntht  1719  nfntht2  1720  19.33  1812  19.33b  1813  dfsb2  2373  mooran2  2528  undif3OLD  3889  undif4  4035  ordelinelOLD  5826  ordssun  5827  tpres  6466  frxp  7287  omopth2  7664  swoord1  7773  swoord2  7774  rankxplim3  8744  fpwwe2lem12  9463  ltapr  9867  zmulcl  11426  nn0lt2  11440  elnn1uz2  11765  mnflt  11957  mnfltpnf  11960  fzm1  12420  expeq0  12890  nn0o1gt2  15097  prm23lt5  15519  vdwlem9  15693  cshwshashlem1  15802  cshwshash  15811  funcres2c  16561  tsrlemax  17220  odlem1  17954  gexlem1  17994  0top  20787  cmpfi  21211  alexsubALTlem3  21853  dyadmbl  23368  plydivex  24052  scvxcvx  24712  gausslemma2dlem0f  25086  nb3grprlem1  26282  1to3vfriswmgr  27144  frgrwopreg  27187  frgrregorufr  27189  frgrregord13  27254  disjunsn  29407  dfon2lem4  31691  dfrdg4  32058  broutsideof2  32229  lineunray  32254  fwddifnp1  32272  meran1  32410  bj-orim2  32541  bj-currypeirce  32544  bj-peircecurry  32545  bj-falor2  32570  bj-sbsb  32824  bj-unrab  32922  wl-orel12  33294  tsor3  33956  paddclN  35128  lcfl6  36789  ifpid3g  37837  ifpim4  37843  rp-fakeanorass  37858  iunrelexp0  37994  clsk1indlem3  38341  19.33-2  38581  ax6e2ndeq  38775  undif3VD  39118  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  disjxp1  39238  stoweidlem26  40243  stoweidlem37  40254  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  salexct  40552  sge0z  40592  sfprmdvdsmersenne  41520  nn0o1gt2ALTV  41605  odd2prm2  41627  even3prm2  41628  stgoldbwt  41664  nrhmzr  41873