Theorem orcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30422. (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  3797  rabsnifsb  4722  n0snor2el  4833  disjprg  5139  propeqop  5512  nf1oconst  7325  poxp  8153  xpord2indlem  8172  naddcllem  8714  unxpwdom2  9628  djuunxp  9961  sornom  10317  fin11a  10423  fin56  10433  fin1a2lem11  10450  axdc3lem2  10491  gchdomtri  10669  0tsk  10795  zmulcl  12666  nn0lt2  12681  nn01to3  12983  xrlttri  13181  xmulpnf1  13316  iccsplit  13525  elfznelfzo  13811  fvf1tp  13829  hashrabsn01  14412  hashsn01  14455  swrdnnn0nd  14694  zsum  15754  sumsplit  15804  zprod  15973  rpnnen2lem11  16260  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  vdwlem6  17024  vdwlem10  17028  cshwshashlem1  17133  basprssdmsets  17259  mreexfidimd  17693  smndex1mgm  18920  sgrp2nmndlem5  18942  symg2bas  19410  psgnunilem1  19511  oppglsm  19660  gsummulgz  19961  prmgrpsimpgd  20134  srgbinomlem4  20226  dvrfval  20402  nrhmzr  20537  lringuplu  20544  cnsubrg  21445  marrepfval  22566  marepvfval  22571  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  fctop  23011  cctop  23013  pptbas  23015  metustto  24566  pmltpclem2  25484  dvne0  26050  taylplem2  26405  taylpfval  26406  dvntaylp0  26414  ang180lem3  26854  scvxcvx  27029  lgsdir2lem5  27373  sltres  27707  addsval  27995  mulsval  28135  mulsproplem13  28154  mulsproplem14  28155  zseo  28406  halfcut  28416  tgbtwnconn1  28583  tgbtwnconn2  28584  tgbtwnconn3  28585  legtrid  28599  hltr  28618  hlbtwn  28619  btwnhl1  28620  btwnhl2  28621  tglineneq  28652  ncolncol  28654  colmid  28696  footexALT  28726  footexlem2  28728  colperpexlem3  28740  colperpex  28741  mideulem2  28742  opphllem  28743  hlpasch  28764  hphl  28779  hypcgrlem1  28807  hypcgrlem2  28808  trgcopy  28812  trgcopyeulem  28813  cgracgr  28826  cgraswap  28828  cgrahl  28835  cgracol  28836  inagflat  28848  inaghl  28853  colinearalglem4  28924  axcontlem3  28981  edglnl  29160  clwlkclwwlklem2a  30017  clwwlknonmpo  30108  trlsegvdeg  30246  nfrgr2v  30291  frgrwopreg  30342  frgrreg  30413  ex-natded5.7  30430  ex-natded5.13  30434  ex-natded9.20  30436  ex-natded9.20-2  30437  padct  32731  f1ocnt  32804  linds2eq  33409  constrelextdg2  33788  submateqlem2  33807  measxun2  34211  measssd  34216  measiun  34219  meascnbl  34220  carsgclctun  34323  satfvsucsuc  35370  fmlasucdisj  35404  satfun  35416  satfv1fvfmla1  35428  2goelgoanfmla1  35429  outsideoftr  36130  lineunray  36148  weiunpo  36466  knoppndvlem6  36518  topdifinffinlem  37348  areacirclem4  37718  smprngopr  38059  tsbi1  38140  tsbi2  38141  lkrshpor  39108  2atmat0  39528  dochsnkrlem3  41473  dvrelog2b  42067  aks4d1p1  42077  aks6d1c2p2  42120  hashnexinjle  42130  unitscyglem2  42197  pell1234qrdich  42872  acongid  42987  acongtr  42990  acongrep  42992  acongeq  42995  jm2.23  43008  jm2.25  43011  jm2.27a  43017  kelac2lem  43076  mendvscafval  43198  fzunt1d  43470  rp-fakeimass  43525  frege106d  43768  clsk1indlem3  44056  nanorxor  44324  undif3VD  44902  refsum2cnlem1  45042  reclt0d  45398  limciccioolb  45636  limcicciooub  45652  wallispilem3  46082  fourierdlem35  46157  fourierdlem80  46201  fourierswlem  46245  fouriersw  46246  dfatprc  47142  nltle2tri  47325  icceuelpartlem  47422  requad01  47608  even3prm2  47706  stgoldbwt  47763  clnbgrvtxel  47816  dfclnbgr6  47842  dfnbgr6  47843  dfsclnbgr6  47844  clnbgrgrim  47902  usgrexmpl2trifr  47996  gpgusgralem  48011  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  ztprmneprm  48263  altgsumbcALT  48269  zlmodzxznm  48414  zlmodzxzldeplem4  48420  reorelicc  48631  prelrrx2b  48635  rrx2plord1  48642  line2x  48675  itscnhlc0xyqsol  48686  itscnhlinecirc02plem1  48703  fvconst0ci  48790  upfval  48933