Theorem olc 882

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 877	1 ⊢ (𝜑 → (𝜓 ∨ 𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm1.4  883  pm2.46  896  norbi  900  pm2.07  916  pm2.41  921  pm1.5  933  biorf  950  pm4.72  964  jaob  976  pm3.48  978  andi  1025  dedlemb  1062  consensus  1068  anifp  1088  cad1  1650  19.33  1919  19.33b  1920  dfsb2  2525  mooran2  2584  undif4  4423  prel12g  4822  ordssun  6482  tpres  7227  fvf1pr  7335  frxp  8162  frxp2  8185  frxp3  8192  omopth2  8617  naddunif  8728  swoord1  8775  swoord2  8776  fpwwe2lem11  10750  ltapr  11154  zmulcl  12769  nn0lt2  12786  elnn1uz2  13076  mnflt  13276  mnfltpnf  13279  fzm1  13765  expeq0  14259  zzlesq  14374  swrdnnn0nd  14831  nn0o1gt2  16577  prm23lt5  17018  vdwlem9  17193  cshwshashlem1  17299  cshwshash  17308  funcres2c  18104  tsrlemax  18786  odlem1  19776  gexlem1  19820  nrhmzr  20816  0top  23328  cmpfi  23753  alexsubALTlem3  24395  dyadmbl  25948  plydivex  26645  scvxcvx  27340  gausslemma2dlem0f  27715  fltoprmlem1  28020  nb3grprlem1  29988  1to3vfriswmgr  30908  frgrwopreg  30951  frgrregorufr  30953  frgrregord13  31024  disjunsn  33257  axprALT2  35815  maxssj0  36005  mirimanofffr  36628  dfon2lem4  36725  dfrdg4  36892  broutsideof2  37064  lineunray  37089  fwddifnp1  37107  meran1  37376  axtco1from2  37440  bj-orim2  37602  bj-peircecurry  37604  bj-falor2  37632  bj-sbsb  37926  bj-unrab  38016  wl-orel12  38634  impprop  38835  tsor3  39272  paddclN  41090  lcfl6  42748  quadfac  43446  sbor2  43455  fsuppind  43809  omcl3g  44526  ifpid3g  44683  ifpim4  44689  rp-fakeanorass  44704  sqrtcval  44831  iunrelexp0  44892  clsk1indlem3  45233  19.33-2  45556  ax6e2ndeq  45731  undif3VD  46053  ax6e2ndeqVD  46080  ax6e2ndeqALT  46102  stoweidlem26  47239  stoweidlem37  47250  fourierswlem  47443  fouriersw  47444  elaa2lem  47446  salexct  47547  sge0z  47588  nfunsnafv2  48498  prproropf1olem4  48791  sfprmdvdsmersenne  48891  nn0o1gt2ALTV  48995  odd2prm2  49019  even3prm2  49020  stgoldbwt  49077  clnbgrel  49129  gpg5nbgrvtx03starlem1  49369  gpg5nbgrvtx03starlem2  49370  gpg5nbgrvtx03starlem3  49371  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  gpg5edgnedg  49431  reorelicc  50025  rrx2plord2  50038  line2y  50070  opth2neg  50141