Theorem orcd 874

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  olcd  875  pm2.47  884  orim12i  909  animorl  980  animorrl  983  cases2ALT  1049  sbc2or  3738  rabsnifsb  4667  n0snor2el  4777  disjprg  5082  propeqop  5455  nf1oconst  7253  poxp  8071  xpord2indlem  8090  naddcllem  8605  unxpwdom2  9496  djuunxp  9836  sornom  10190  fin11a  10296  fin56  10306  fin1a2lem11  10323  axdc3lem2  10364  gchdomtri  10543  0tsk  10669  zmulcl  12567  nn0lt2  12583  nn01to3  12882  xrlttri  13081  xmulpnf1  13217  iccsplit  13429  elfznelfzo  13719  fvf1tp  13739  hashrabsn01  14326  hashsn01  14369  swrdnnn0nd  14610  zsum  15671  sumsplit  15721  zprod  15893  rpnnen2lem11  16182  lcmfunsnlem2lem1  16598  lcmfunsnlem2  16600  vdwlem6  16948  vdwlem10  16952  cshwshashlem1  17057  basprssdmsets  17182  mreexfidimd  17607  chnccat  18583  smndex1mgm  18869  sgrp2nmndlem5  18891  symg2bas  19359  psgnunilem1  19459  oppglsm  19608  gsummulgz  19909  prmgrpsimpgd  20082  srgbinomlem4  20201  dvrfval  20373  nrhmzr  20505  lringuplu  20512  cnsubrg  21417  marrepfval  22535  marepvfval  22540  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  fctop  22979  cctop  22981  pptbas  22983  metustto  24528  pmltpclem2  25426  dvne0  25988  taylplem2  26340  taylpfval  26341  dvntaylp0  26349  ang180lem3  26788  scvxcvx  26963  lgsdir2lem5  27306  ltsres  27640  addsval  27968  mulsval  28115  mulsproplem13  28134  mulsproplem14  28135  oncutlt  28270  n0fincut  28361  zseo  28428  halfcut  28464  z12zsodd  28488  tgbtwnconn1  28657  tgbtwnconn2  28658  tgbtwnconn3  28659  legtrid  28673  hltr  28692  hlbtwn  28693  btwnhl1  28694  btwnhl2  28695  tglineneq  28726  ncolncol  28728  colmid  28770  footexALT  28800  footexlem2  28802  colperpexlem3  28814  colperpex  28815  mideulem2  28816  opphllem  28817  hlpasch  28838  hphl  28853  hypcgrlem1  28881  hypcgrlem2  28882  trgcopy  28886  trgcopyeulem  28887  cgracgr  28900  cgraswap  28902  cgrahl  28909  cgracol  28910  inagflat  28922  inaghl  28927  colinearalglem4  28992  axcontlem3  29049  edglnl  29226  clwlkclwwlklem2a  30083  clwwlknonmpo  30174  trlsegvdeg  30312  nfrgr2v  30357  frgrwopreg  30408  frgrreg  30479  ex-natded5.7  30496  ex-natded5.13  30500  ex-natded9.20  30502  ex-natded9.20-2  30503  f1ocnt  32888  linds2eq  33456  constrelextdg2  33907  submateqlem2  33968  measxun2  34370  measssd  34375  measiun  34378  meascnbl  34379  carsgclctun  34481  satfvsucsuc  35563  fmlasucdisj  35597  satfun  35609  satfv1fvfmla1  35621  2goelgoanfmla1  35622  outsideoftr  36327  lineunray  36345  weiunpo  36663  knoppndvlem6  36793  topdifinffinlem  37677  areacirclem4  38046  smprngopr  38387  tsbi1  38468  tsbi2  38469  lkrshpor  39567  2atmat0  39986  dochsnkrlem3  41931  dvrelog2b  42519  aks4d1p1  42529  aks6d1c2p2  42572  hashnexinjle  42582  unitscyglem2  42649  pell1234qrdich  43307  acongid  43421  acongtr  43424  acongrep  43426  acongeq  43429  jm2.23  43442  jm2.25  43445  jm2.27a  43451  kelac2lem  43510  mendvscafval  43632  fzunt1d  43902  rp-fakeimass  43957  frege106d  44200  clsk1indlem3  44488  nanorxor  44750  undif3VD  45326  refsum2cnlem1  45486  reclt0d  45834  limciccioolb  46069  limcicciooub  46083  wallispilem3  46513  fourierdlem35  46588  fourierdlem80  46632  fourierswlem  46676  fouriersw  46677  squeezedltsq  47334  dfatprc  47590  nltle2tri  47773  icceuelpartlem  47907  requad01  48109  even3prm2  48207  stgoldbwt  48264  clnbgrvtxel  48317  dfclnbgr6  48344  dfnbgr6  48345  dfsclnbgr6  48346  clnbgrgrim  48422  usgrexmpl2trifr  48525  gpgusgralem  48544  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg3nbgrvtx0  48564  gpg3nbgrvtx0ALT  48565  gpg3nbgrvtx1  48566  gpg5edgnedg  48618  ztprmneprm  48835  altgsumbcALT  48841  zlmodzxznm  48985  zlmodzxzldeplem4  48991  reorelicc  49198  prelrrx2b  49202  rrx2plord1  49209  line2x  49242  itscnhlc0xyqsol  49253  itscnhlinecirc02plem1  49270  fvconst0ci  49378  upfval  49663