Theorem olc 398

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

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

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 196  df-or 384

This theorem is referenced by:  pm1.4  400  pm2.07  410  pm2.46  412  biorf  419  pm1.5  543  pm2.41  595  jaob  818  pm3.48  874  norbi  900  andi  907  pm4.72  916  consensus  990  dedlemb  994  anifp  1014  cad1  1546  nfntht  1710  nfntht2  1711  19.33  1801  19.33b  1802  dfsb2  2361  mooran2  2516  undif3OLD  3848  undif4  3987  ordelinelOLD  5743  ordssun  5744  tpres  6371  frxp  7174  omopth2  7551  swoord1  7660  swoord2  7661  rankxplim3  8627  fpwwe2lem12  9342  ltapr  9746  zmulcl  11303  nn0lt2  11317  elnn1uz2  11641  mnflt  11833  mnfltpnf  11836  fzm1  12289  expeq0  12752  nn0o1gt2  14935  prm23lt5  15357  vdwlem9  15531  cshwshashlem1  15640  cshwshash  15649  funcres2c  16384  tsrlemax  17043  odlem1  17777  gexlem1  17817  0top  20598  cmpfi  21021  alexsubALTlem3  21663  dyadmbl  23174  plydivex  23856  scvxcvx  24512  gausslemma2dlem0f  24886  nb3graprlem1  25980  uvtx01vtx  26020  1to3vfriswmgra  26534  frgraregorufr  26580  frgraregord13  26646  disjunsn  28789  dfon2lem4  30935  sltsgn1  31058  sltsgn2  31059  dfrdg4  31228  broutsideof2  31399  lineunray  31424  fwddifnp1  31442  meran1  31580  bj-orim2  31711  bj-currypeirce  31714  bj-peircecurry  31715  bj-falor2  31743  bj-nfntht  31770  bj-nfntht2  31771  bj-sbsb  32012  bj-unrab  32114  wl-orel12  32473  tsor3  33126  paddclN  34146  lcfl6  35807  ifpid3g  36856  ifpim4  36862  rp-fakeanorass  36877  iunrelexp0  37013  clsk1indlem3  37361  19.33-2  37603  ax6e2ndeq  37796  undif3VD  38140  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  disjxp1  38263  nelpr2  38288  stoweidlem26  38919  stoweidlem37  38930  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  salexct  39228  sge0z  39268  sfprmdvdsmersenne  40058  nn0o1gt2ALTV  40143  stgoldbwt  40198  nb3grprlem1  40608  1to3vfriswmgr  41450  frgrregorufr  41490  av-frgraregord13  41550  nrhmzr  41663