Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30365. (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 867	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  olcd  874  pm2.47  883  orim12i  908  animorl  979  animorrl  982  cases2ALT  1048  sbc2or  3753  rabsnifsb  4676  n0snor2el  4787  disjprg  5091  propeqop  5454  nf1oconst  7246  poxp  8068  xpord2indlem  8087  naddcllem  8601  unxpwdom2  9499  djuunxp  9836  sornom  10190  fin11a  10296  fin56  10306  fin1a2lem11  10323  axdc3lem2  10364  gchdomtri  10542  0tsk  10668  zmulcl  12542  nn0lt2  12557  nn01to3  12860  xrlttri  13059  xmulpnf1  13194  iccsplit  13406  elfznelfzo  13693  fvf1tp  13711  hashrabsn01  14298  hashsn01  14341  swrdnnn0nd  14581  zsum  15643  sumsplit  15693  zprod  15862  rpnnen2lem11  16151  lcmfunsnlem2lem1  16567  lcmfunsnlem2  16569  vdwlem6  16916  vdwlem10  16920  cshwshashlem1  17025  basprssdmsets  17150  mreexfidimd  17574  smndex1mgm  18799  sgrp2nmndlem5  18821  symg2bas  19290  psgnunilem1  19390  oppglsm  19539  gsummulgz  19840  prmgrpsimpgd  20013  srgbinomlem4  20132  dvrfval  20305  nrhmzr  20440  lringuplu  20447  cnsubrg  21352  marrepfval  22463  marepvfval  22468  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  fctop  22907  cctop  22909  pptbas  22911  metustto  24457  pmltpclem2  25366  dvne0  25932  taylplem2  26287  taylpfval  26288  dvntaylp0  26296  ang180lem3  26737  scvxcvx  26912  lgsdir2lem5  27256  sltres  27590  addsval  27892  mulsval  28035  mulsproplem13  28054  mulsproplem14  28055  onscutlt  28188  n0sfincut  28269  zseo  28332  halfcut  28364  zs12zodd  28377  tgbtwnconn1  28538  tgbtwnconn2  28539  tgbtwnconn3  28540  legtrid  28554  hltr  28573  hlbtwn  28574  btwnhl1  28575  btwnhl2  28576  tglineneq  28607  ncolncol  28609  colmid  28651  footexALT  28681  footexlem2  28683  colperpexlem3  28695  colperpex  28696  mideulem2  28697  opphllem  28698  hlpasch  28719  hphl  28734  hypcgrlem1  28762  hypcgrlem2  28763  trgcopy  28767  trgcopyeulem  28768  cgracgr  28781  cgraswap  28783  cgrahl  28790  cgracol  28791  inagflat  28803  inaghl  28808  colinearalglem4  28872  axcontlem3  28929  edglnl  29106  clwlkclwwlklem2a  29960  clwwlknonmpo  30051  trlsegvdeg  30189  nfrgr2v  30234  frgrwopreg  30285  frgrreg  30356  ex-natded5.7  30373  ex-natded5.13  30377  ex-natded9.20  30379  ex-natded9.20-2  30380  padct  32676  f1ocnt  32758  linds2eq  33331  constrelextdg2  33716  submateqlem2  33777  measxun2  34179  measssd  34184  measiun  34187  meascnbl  34188  carsgclctun  34291  satfvsucsuc  35340  fmlasucdisj  35374  satfun  35386  satfv1fvfmla1  35398  2goelgoanfmla1  35399  outsideoftr  36105  lineunray  36123  weiunpo  36441  knoppndvlem6  36493  topdifinffinlem  37323  areacirclem4  37693  smprngopr  38034  tsbi1  38115  tsbi2  38116  lkrshpor  39088  2atmat0  39508  dochsnkrlem3  41453  dvrelog2b  42042  aks4d1p1  42052  aks6d1c2p2  42095  hashnexinjle  42105  unitscyglem2  42172  pell1234qrdich  42837  acongid  42951  acongtr  42954  acongrep  42956  acongeq  42959  jm2.23  42972  jm2.25  42975  jm2.27a  42981  kelac2lem  43040  mendvscafval  43162  fzunt1d  43433  rp-fakeimass  43488  frege106d  43731  clsk1indlem3  44019  nanorxor  44281  undif3VD  44858  refsum2cnlem1  45018  reclt0d  45370  limciccioolb  45606  limcicciooub  45622  wallispilem3  46052  fourierdlem35  46127  fourierdlem80  46171  fourierswlem  46215  fouriersw  46216  squeezedltsq  46874  dfatprc  47118  nltle2tri  47301  icceuelpartlem  47423  requad01  47609  even3prm2  47707  stgoldbwt  47764  clnbgrvtxel  47817  dfclnbgr6  47844  dfnbgr6  47845  dfsclnbgr6  47846  clnbgrgrim  47922  usgrexmpl2trifr  48025  gpgusgralem  48044  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg3nbgrvtx0  48064  gpg3nbgrvtx0ALT  48065  gpg3nbgrvtx1  48066  gpg5edgnedg  48118  ztprmneprm  48335  altgsumbcALT  48341  zlmodzxznm  48486  zlmodzxzldeplem4  48492  reorelicc  48699  prelrrx2b  48703  rrx2plord1  48710  line2x  48743  itscnhlc0xyqsol  48754  itscnhlinecirc02plem1  48771  fvconst0ci  48879  upfval  49165