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  1649  19.33  1916  19.33b  1917  dfsb2  2522  mooran2  2581  undif4  4419  prel12g  4823  ordssun  6467  tpres  7207  fvf1pr  7315  frxp  8138  frxp2  8161  frxp3  8168  omopth2  8592  naddunif  8703  swoord1  8750  swoord2  8751  fpwwe2lem11  10726  ltapr  11130  zmulcl  12745  nn0lt2  12762  elnn1uz2  13052  mnflt  13252  mnfltpnf  13255  fzm1  13741  expeq0  14235  zzlesq  14350  swrdnnn0nd  14806  nn0o1gt2  16551  prm23lt5  16992  vdwlem9  17167  cshwshashlem1  17273  cshwshash  17282  funcres2c  18078  tsrlemax  18760  odlem1  19749  gexlem1  19793  nrhmzr  20789  0top  23301  cmpfi  23726  alexsubALTlem3  24368  dyadmbl  25921  plydivex  26618  scvxcvx  27313  gausslemma2dlem0f  27688  fltoprmlem1  27993  nb3grprlem1  29961  1to3vfriswmgr  30881  frgrwopreg  30924  frgrregorufr  30926  frgrregord13  30997  disjunsn  33188  axprALT2  35734  dfon2lem4  36548  dfrdg4  36715  broutsideof2  36887  lineunray  36912  fwddifnp1  36930  meran1  37199  axtco1from2  37263  bj-orim2  37425  bj-peircecurry  37427  bj-falor2  37455  bj-sbsb  37749  bj-unrab  37839  wl-orel12  38444  impprop  38645  tsor3  39082  paddclN  40900  lcfl6  42558  quadfac  43256  sbor2  43265  fsuppind  43619  omcl3g  44336  ifpid3g  44493  ifpim4  44499  rp-fakeanorass  44514  sqrtcval  44641  iunrelexp0  44702  clsk1indlem3  45043  19.33-2  45366  ax6e2ndeq  45542  undif3VD  45864  ax6e2ndeqVD  45891  ax6e2ndeqALT  45913  stoweidlem26  47036  stoweidlem37  47047  fourierswlem  47240  fouriersw  47241  elaa2lem  47243  salexct  47344  sge0z  47385  nfunsnafv2  48295  prproropf1olem4  48588  sfprmdvdsmersenne  48688  nn0o1gt2ALTV  48792  odd2prm2  48816  even3prm2  48817  stgoldbwt  48874  clnbgrel  48926  gpg5nbgrvtx03starlem1  49166  gpg5nbgrvtx03starlem2  49167  gpg5nbgrvtx03starlem3  49168  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem2  49170  gpg5nbgrvtx13starlem3  49171  gpg5edgnedg  49228  reorelicc  49822  rrx2plord2  49834  line2y  49867  opth2neg  49937