Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30384. (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  3774  rabsnifsb  4698  n0snor2el  4809  disjprg  5115  propeqop  5482  nf1oconst  7298  poxp  8127  xpord2indlem  8146  naddcllem  8688  unxpwdom2  9602  djuunxp  9935  sornom  10291  fin11a  10397  fin56  10407  fin1a2lem11  10424  axdc3lem2  10465  gchdomtri  10643  0tsk  10769  zmulcl  12641  nn0lt2  12656  nn01to3  12957  xrlttri  13155  xmulpnf1  13290  iccsplit  13502  elfznelfzo  13788  fvf1tp  13806  hashrabsn01  14391  hashsn01  14434  swrdnnn0nd  14674  zsum  15734  sumsplit  15784  zprod  15953  rpnnen2lem11  16242  lcmfunsnlem2lem1  16657  lcmfunsnlem2  16659  vdwlem6  17006  vdwlem10  17010  cshwshashlem1  17115  basprssdmsets  17240  mreexfidimd  17662  smndex1mgm  18885  sgrp2nmndlem5  18907  symg2bas  19374  psgnunilem1  19474  oppglsm  19623  gsummulgz  19924  prmgrpsimpgd  20097  srgbinomlem4  20189  dvrfval  20362  nrhmzr  20497  lringuplu  20504  cnsubrg  21395  marrepfval  22498  marepvfval  22503  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  fctop  22942  cctop  22944  pptbas  22946  metustto  24492  pmltpclem2  25402  dvne0  25968  taylplem2  26323  taylpfval  26324  dvntaylp0  26332  ang180lem3  26773  scvxcvx  26948  lgsdir2lem5  27292  sltres  27626  addsval  27921  mulsval  28064  mulsproplem13  28083  mulsproplem14  28084  onscutlt  28217  n0sfincut  28298  zseo  28360  halfcut  28385  tgbtwnconn1  28554  tgbtwnconn2  28555  tgbtwnconn3  28556  legtrid  28570  hltr  28589  hlbtwn  28590  btwnhl1  28591  btwnhl2  28592  tglineneq  28623  ncolncol  28625  colmid  28667  footexALT  28697  footexlem2  28699  colperpexlem3  28711  colperpex  28712  mideulem2  28713  opphllem  28714  hlpasch  28735  hphl  28750  hypcgrlem1  28778  hypcgrlem2  28779  trgcopy  28783  trgcopyeulem  28784  cgracgr  28797  cgraswap  28799  cgrahl  28806  cgracol  28807  inagflat  28819  inaghl  28824  colinearalglem4  28888  axcontlem3  28945  edglnl  29122  clwlkclwwlklem2a  29979  clwwlknonmpo  30070  trlsegvdeg  30208  nfrgr2v  30253  frgrwopreg  30304  frgrreg  30375  ex-natded5.7  30392  ex-natded5.13  30396  ex-natded9.20  30398  ex-natded9.20-2  30399  padct  32697  f1ocnt  32779  linds2eq  33396  constrelextdg2  33781  submateqlem2  33839  measxun2  34241  measssd  34246  measiun  34249  meascnbl  34250  carsgclctun  34353  satfvsucsuc  35387  fmlasucdisj  35421  satfun  35433  satfv1fvfmla1  35445  2goelgoanfmla1  35446  outsideoftr  36147  lineunray  36165  weiunpo  36483  knoppndvlem6  36535  topdifinffinlem  37365  areacirclem4  37735  smprngopr  38076  tsbi1  38157  tsbi2  38158  lkrshpor  39125  2atmat0  39545  dochsnkrlem3  41490  dvrelog2b  42079  aks4d1p1  42089  aks6d1c2p2  42132  hashnexinjle  42142  unitscyglem2  42209  pell1234qrdich  42884  acongid  42999  acongtr  43002  acongrep  43004  acongeq  43007  jm2.23  43020  jm2.25  43023  jm2.27a  43029  kelac2lem  43088  mendvscafval  43210  fzunt1d  43481  rp-fakeimass  43536  frege106d  43779  clsk1indlem3  44067  nanorxor  44329  undif3VD  44906  refsum2cnlem1  45061  reclt0d  45414  limciccioolb  45650  limcicciooub  45666  wallispilem3  46096  fourierdlem35  46171  fourierdlem80  46215  fourierswlem  46259  fouriersw  46260  squeezedltsq  46918  dfatprc  47159  nltle2tri  47342  icceuelpartlem  47449  requad01  47635  even3prm2  47733  stgoldbwt  47790  clnbgrvtxel  47843  dfclnbgr6  47869  dfnbgr6  47870  dfsclnbgr6  47871  clnbgrgrim  47947  usgrexmpl2trifr  48041  gpgusgralem  48060  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  gpg3nbgrvtx0  48078  gpg3nbgrvtx0ALT  48079  gpg3nbgrvtx1  48080  ztprmneprm  48322  altgsumbcALT  48328  zlmodzxznm  48473  zlmodzxzldeplem4  48479  reorelicc  48690  prelrrx2b  48694  rrx2plord1  48701  line2x  48734  itscnhlc0xyqsol  48745  itscnhlinecirc02plem1  48762  fvconst0ci  48866  upfval  49111