Theorem orcd 870

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

Syntax hints:   → wi 4   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  olcd  871  pm2.47  881  orim12i  906  animorl  975  animorrl  978  cases2ALT  1046  sbc2or  3726  rabsnifsb  4659  n0snor2el  4765  disjprgw  5070  disjprg  5071  propeqop  5422  nf1oconst  7186  poxp  7978  unxpwdom2  9356  djuunxp  9688  sornom  10042  fin11a  10148  fin56  10158  fin1a2lem11  10175  axdc3lem2  10216  gchdomtri  10394  0tsk  10520  zmulcl  12378  nn0lt2  12392  nn01to3  12690  xrlttri  12882  xmulpnf1  13017  iccsplit  13226  elfznelfzo  13501  hashrabsn01  14097  hashsn01  14140  swrdnnn0nd  14378  zsum  15439  sumsplit  15489  zprod  15656  rpnnen2lem11  15942  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  vdwlem6  16696  vdwlem10  16700  cshwshashlem1  16806  basprssdmsets  16934  mreexfidimd  17368  smndex1mgm  18555  sgrp2nmndlem5  18577  symg2bas  19009  psgnunilem1  19110  oppglsm  19256  gsummulgz  19553  prmgrpsimpgd  19726  srgbinomlem4  19788  dvrfval  19935  cnsubrg  20667  marrepfval  21718  marepvfval  21723  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  fctop  22163  cctop  22165  pptbas  22167  metustto  23718  pmltpclem2  24622  dvne0  25184  taylplem2  25532  taylpfval  25533  dvntaylp0  25540  ang180lem3  25970  scvxcvx  26144  lgsdir2lem5  26486  tgbtwnconn1  26945  tgbtwnconn2  26946  tgbtwnconn3  26947  legtrid  26961  hltr  26980  hlbtwn  26981  btwnhl1  26982  btwnhl2  26983  tglineneq  27014  ncolncol  27016  colmid  27058  footexALT  27088  footexlem2  27090  colperpexlem3  27102  colperpex  27103  mideulem2  27104  opphllem  27105  hlpasch  27126  hphl  27141  hypcgrlem1  27169  hypcgrlem2  27170  trgcopy  27174  trgcopyeulem  27175  cgracgr  27188  cgraswap  27190  cgrahl  27197  cgracol  27198  inagflat  27210  inaghl  27215  colinearalglem4  27286  axcontlem3  27343  edglnl  27522  clwlkclwwlklem2a  28371  clwwlknonmpo  28462  trlsegvdeg  28600  nfrgr2v  28645  frgrwopreg  28696  frgrreg  28767  ex-natded5.7  28784  ex-natded5.13  28788  ex-natded9.20  28790  ex-natded9.20-2  28791  padct  31063  f1ocnt  31132  linds2eq  31584  submateqlem2  31767  measxun2  32187  measssd  32192  measiun  32195  meascnbl  32196  carsgclctun  32297  satfvsucsuc  33336  fmlasucdisj  33370  satfun  33382  satfv1fvfmla1  33394  2goelgoanfmla1  33395  xpord2ind  33803  naddcllem  33840  sltres  33874  addsval  34135  outsideoftr  34440  lineunray  34458  knoppndvlem6  34706  topdifinffinlem  35527  areacirclem4  35877  smprngopr  36219  tsbi1  36300  tsbi2  36301  lkrshpor  37128  2atmat0  37547  dochsnkrlem3  39492  dvrelog2b  40081  aks4d1p1  40091  pell1234qrdich  40690  acongid  40804  acongtr  40807  acongrep  40809  acongeq  40812  jm2.23  40825  jm2.25  40828  jm2.27a  40834  kelac2lem  40896  mendvscafval  41022  fzunt1d  41071  rp-fakeimass  41126  frege106d  41370  clsk1indlem3  41660  nanorxor  41930  undif3VD  42509  refsum2cnlem1  42587  reclt0d  42933  limciccioolb  43169  limcicciooub  43185  wallispilem3  43615  fourierdlem35  43690  fourierdlem80  43734  fourierswlem  43778  fouriersw  43779  dfatprc  44633  nltle2tri  44816  icceuelpartlem  44898  requad01  45084  even3prm2  45182  stgoldbwt  45239  isomuspgrlem1  45290  nrhmzr  45442  ztprmneprm  45694  altgsumbcALT  45700  zlmodzxznm  45849  zlmodzxzldeplem4  45855  reorelicc  46067  prelrrx2b  46071  rrx2plord1  46078  line2x  46111  itscnhlc0xyqsol  46122  itscnhlinecirc02plem1  46139  fvconst0ci  46197