Theorem orcd 887

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  olcd  888  pm2.47  897  orim12i  922  animorl  993  animorrl  996  cases2ALT  1064  sbc2or  3748  rabsnifsb  4683  n0snor2el  4793  disjprg  5099  propeqop  5479  nf1oconst  7305  poxp  8129  xpord2indlem  8148  naddcllem  8669  unxpwdom2  9566  djuunxp  9983  sornom  10336  fin11a  10442  fin56  10452  fin1a2lem11  10469  axdc3lem2  10510  gchdomtri  10695  0tsk  10821  zmulcl  12726  nn0lt2  12743  nn01to3  13049  xrlttri  13249  xmulpnf1  13385  iccsplit  13597  elfznelfzo  13888  fvf1tp  13909  hashrabsn01  14497  hashsn01  14541  swrdnnn0nd  14786  zsum  15864  sumsplit  15914  zprod  16084  rpnnen2lem11  16372  lcmfunsnlem2lem1  16793  lcmfunsnlem2  16795  vdwlem6  17144  vdwlem10  17148  cshwshashlem1  17253  basprssdmsets  17379  mreexfidimd  17804  chnccat  18780  smndex1mgm  19086  sgrp2nmndlem5  19108  symg2bas  19587  psgnunilem1  19687  oppglsm  19836  gsummulgz  20137  prmgrpsimpgd  20310  srgbinomlem4  20435  dvrfval  20612  nrhmzr  20769  lringuplu  20776  isfieldidl  21520  cnsubrg  21713  marrepfval  22855  marepvfval  22860  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  fctop  23302  cctop  23304  pptbas  23306  metustto  24852  pmltpclem2  25750  dvne0  26311  taylplem2  26673  taylpfval  26674  dvntaylp0  26681  ang180lem3  27121  scvxcvx  27295  lgsdir2lem5  27638  fltoprmlem1  27975  ltsres  28001  addsval  28330  mulsval  28477  mulsproplem13  28496  mulsproplem14  28497  oncutlt  28632  n0fincut  28723  zseo  28790  halfcut  28826  z12zsodd  28850  tgbtwnconn1  29020  tgbtwnconn2  29021  tgbtwnconn3  29022  legtrid  29036  hltr  29058  hlbtwn  29059  btwnhl1  29060  btwnhl2  29061  tglineneq  29095  ncolncol  29097  colmid  29142  symquadprlnglem  29147  footexALT  29175  footexlem2  29177  colperpexlem3  29190  colperpex  29191  mideulem2  29192  opphllem  29193  hlpasch  29216  hphl  29231  hlopp  29232  lnincplng  29244  plngrotlem2  29248  symquadmid  29286  hypcgrlem1  29287  hypcgrlem2  29288  trgcopy  29293  trgcopyeulem  29294  cgracgr  29307  cgraswap  29309  cgrahl  29317  cgracol  29318  ragcgra  29325  cgrarag  29326  inagflat  29341  inaghl  29346  angmgmaddeu1  29361  angmgmaddcpbl  29372  prlngref  29400  symquadprlng  29422  colinearalglem4  29469  axcontlem3  29526  edglnl  29703  clwlkclwwlklem2a  30571  clwwlknonmpo  30662  trlsegvdeg  30810  nfrgr2v  30855  frgrwopreg  30906  frgrreg  30977  ex-natded5.7  30994  ex-natded5.13  30998  ex-natded9.20  31000  ex-natded9.20-2  31001  f1ocnt  33374  linds2eq  33918  constrelextdg2  34361  submateqlem2  34422  measxun2  34825  measssd  34830  measiun  34833  meascnbl  34834  carsgclctun  34936  satfvsucsuc  36099  fmlasucdisj  36133  satfun  36145  satfv1fvfmla1  36157  2goelgoanfmla1  36158  outsideoftr  36864  lineunray  36882  weiunpo  37223  knoppndvlem6  37353  topdifinffinlem  38238  areacirclem4  38597  negprop  38611  impprop  38612  smprngopr  38954  tsbi1  39033  tsbi2  39034  lkrshpor  40132  2atmat0  40551  dochsnkrlem3  42496  dvrelog2b  43084  aks4d1p1  43094  aks6d1c2p2  43137  hashnexinjle  43147  unitscyglem2  43214  pell1234qrdich  43821  acongid  43935  acongtr  43938  acongrep  43940  acongeq  43943  jm2.23  43956  jm2.25  43959  jm2.27a  43965  kelac2lem  44024  mendvscafval  44146  fzunt1d  44416  rp-fakeimass  44471  frege106d  44714  clsk1indlem3  45002  nanorxor  45248  undif3VD  45823  refsum2cnlem1  45997  reclt0d  46342  limciccioolb  46577  limcicciooub  46591  wallispilem3  47021  fourierdlem35  47096  fourierdlem80  47140  fourierswlem  47184  fouriersw  47185  dfatprc  48144  nltle2tri  48327  icceuelpartlem  48461  requad01  48663  even3prm2  48761  stgoldbwt  48818  clnbgrvtxel  48871  dfclnbgr6  48898  dfnbgr6  48899  dfsclnbgr6  48900  clnbgrgrim  48976  usgrexmpl2trifr  49079  gpgusgralem  49098  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpg3nbgrvtx0  49118  gpg3nbgrvtx0ALT  49119  gpg3nbgrvtx1  49120  gpg5edgnedg  49172  smprngprmrng  49380  ztprmneprm  49403  altgsumbcALT  49409  zlmodzxznm  49553  zlmodzxzldeplem4  49559  reorelicc  49766  prelrrx2b  49770  rrx2plord1  49777  line2x  49810  itscnhlc0xyqsol  49821  itscnhlinecirc02plem1  49838  fvconst0ci  49943  upfval  50228