Theorem orcd 879

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30498. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
orcd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 ⊢ (𝜑 → 𝜓)
2		orc 873	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  olcd  880  pm2.47  889  orim12i  914  animorl  985  animorrl  988  cases2ALT  1054  sbc2or  3739  rabsnifsb  4661  n0snor2el  4771  disjprg  5075  propeqop  5455  nf1oconst  7256  poxp  8075  xpord2indlem  8094  naddcllem  8609  unxpwdom2  9500  djuunxp  9843  sornom  10197  fin11a  10303  fin56  10313  fin1a2lem11  10330  axdc3lem2  10371  gchdomtri  10550  0tsk  10676  zmulcl  12574  nn0lt2  12590  nn01to3  12889  xrlttri  13088  xmulpnf1  13224  iccsplit  13436  elfznelfzo  13726  fvf1tp  13746  hashrabsn01  14333  hashsn01  14376  swrdnnn0nd  14617  zsum  15678  sumsplit  15728  zprod  15900  rpnnen2lem11  16189  lcmfunsnlem2lem1  16605  lcmfunsnlem2  16607  vdwlem6  16955  vdwlem10  16959  cshwshashlem1  17064  basprssdmsets  17189  mreexfidimd  17614  chnccat  18590  smndex1mgm  18876  sgrp2nmndlem5  18898  symg2bas  19366  psgnunilem1  19466  oppglsm  19615  gsummulgz  19916  prmgrpsimpgd  20089  srgbinomlem4  20208  dvrfval  20380  nrhmzr  20516  lringuplu  20523  cnsubrg  21409  marrepfval  22550  marepvfval  22555  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  fctop  22994  cctop  22996  pptbas  22998  metustto  24543  pmltpclem2  25441  dvne0  26003  taylplem2  26354  taylpfval  26355  dvntaylp0  26362  ang180lem3  26800  scvxcvx  26974  lgsdir2lem5  27317  ltsres  27651  addsval  27979  mulsval  28126  mulsproplem13  28145  mulsproplem14  28146  oncutlt  28281  n0fincut  28372  zseo  28439  halfcut  28475  z12zsodd  28499  tgbtwnconn1  28668  tgbtwnconn2  28669  tgbtwnconn3  28670  legtrid  28684  hltr  28703  hlbtwn  28704  btwnhl1  28705  btwnhl2  28706  tglineneq  28737  ncolncol  28739  colmid  28781  footexALT  28811  footexlem2  28813  colperpexlem3  28825  colperpex  28826  mideulem2  28827  opphllem  28828  hlpasch  28849  hphl  28864  hypcgrlem1  28892  hypcgrlem2  28893  trgcopy  28897  trgcopyeulem  28898  cgracgr  28911  cgraswap  28913  cgrahl  28920  cgracol  28921  inagflat  28933  inaghl  28938  colinearalglem4  29003  axcontlem3  29060  edglnl  29237  clwlkclwwlklem2a  30093  clwwlknonmpo  30184  trlsegvdeg  30322  nfrgr2v  30367  frgrwopreg  30418  frgrreg  30489  ex-natded5.7  30506  ex-natded5.13  30510  ex-natded9.20  30512  ex-natded9.20-2  30513  f1ocnt  32899  linds2eq  33471  constrelextdg2  33938  submateqlem2  33999  measxun2  34401  measssd  34406  measiun  34409  meascnbl  34410  carsgclctun  34512  satfvsucsuc  35600  fmlasucdisj  35634  satfun  35646  satfv1fvfmla1  35658  2goelgoanfmla1  35659  outsideoftr  36364  lineunray  36382  weiunpo  36700  knoppndvlem6  36830  topdifinffinlem  37716  areacirclem4  38085  smprngopr  38426  tsbi1  38507  tsbi2  38508  lkrshpor  39606  2atmat0  40025  dochsnkrlem3  41970  dvrelog2b  42558  aks4d1p1  42568  aks6d1c2p2  42611  hashnexinjle  42621  unitscyglem2  42688  pell1234qrdich  43313  acongid  43427  acongtr  43430  acongrep  43432  acongeq  43435  jm2.23  43448  jm2.25  43451  jm2.27a  43457  kelac2lem  43516  mendvscafval  43638  fzunt1d  43908  rp-fakeimass  43963  frege106d  44206  clsk1indlem3  44494  nanorxor  44756  undif3VD  45332  refsum2cnlem1  45492  reclt0d  45838  limciccioolb  46073  limcicciooub  46087  wallispilem3  46517  fourierdlem35  46592  fourierdlem80  46636  fourierswlem  46680  fouriersw  46681  squeezedltsq  47340  dfatprc  47600  nltle2tri  47783  icceuelpartlem  47917  requad01  48119  even3prm2  48217  stgoldbwt  48274  clnbgrvtxel  48327  dfclnbgr6  48354  dfnbgr6  48355  dfsclnbgr6  48356  clnbgrgrim  48432  usgrexmpl2trifr  48535  gpgusgralem  48554  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg3nbgrvtx0  48574  gpg3nbgrvtx0ALT  48575  gpg3nbgrvtx1  48576  gpg5edgnedg  48628  ztprmneprm  48845  altgsumbcALT  48851  zlmodzxznm  48995  zlmodzxzldeplem4  49001  reorelicc  49208  prelrrx2b  49212  rrx2plord1  49219  line2x  49252  itscnhlc0xyqsol  49263  itscnhlinecirc02plem1  49280  fvconst0ci  49388  upfval  49673