Theorem orcd 886

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  olcd  887  pm2.47  896  orim12i  921  animorl  993  animorrl  996  cases2ALT  1062  sbc2or  3756  rabsnifsb  4684  n0snor2el  4793  disjprg  5100  propeqop  5480  nf1oconst  7293  poxp  8112  xpord2indlem  8131  naddcllem  8650  unxpwdom2  9538  djuunxp  9895  sornom  10249  fin11a  10355  fin56  10365  fin1a2lem11  10382  axdc3lem2  10423  gchdomtri  10602  0tsk  10728  zmulcl  12631  nn0lt2  12647  nn01to3  12953  xrlttri  13152  xmulpnf1  13288  iccsplit  13500  elfznelfzo  13790  fvf1tp  13810  hashrabsn01  14397  hashsn01  14441  swrdnnn0nd  14682  zsum  15757  sumsplit  15807  zprod  15979  rpnnen2lem11  16268  lcmfunsnlem2lem1  16684  lcmfunsnlem2  16686  vdwlem6  17034  vdwlem10  17038  cshwshashlem1  17143  basprssdmsets  17269  mreexfidimd  17694  chnccat  18670  smndex1mgm  18957  sgrp2nmndlem5  18979  symg2bas  19451  psgnunilem1  19551  oppglsm  19700  gsummulgz  20001  prmgrpsimpgd  20174  srgbinomlem4  20299  dvrfval  20472  nrhmzr  20610  lringuplu  20617  cnsubrg  21534  marrepfval  22674  marepvfval  22679  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  fctop  23118  cctop  23120  pptbas  23122  metustto  24667  pmltpclem2  25565  dvne0  26127  taylplem2  26481  taylpfval  26482  dvntaylp0  26489  ang180lem3  26930  scvxcvx  27104  lgsdir2lem5  27447  ltsres  27780  addsval  28109  mulsval  28256  mulsproplem13  28275  mulsproplem14  28276  oncutlt  28411  n0fincut  28502  zseo  28569  halfcut  28605  z12zsodd  28629  tgbtwnconn1  28798  tgbtwnconn2  28799  tgbtwnconn3  28800  legtrid  28814  hltr  28833  hlbtwn  28834  btwnhl1  28835  btwnhl2  28836  tglineneq  28868  ncolncol  28870  colmid  28915  footexALT  28945  footexlem2  28947  colperpexlem3  28959  colperpex  28960  mideulem2  28961  opphllem  28962  hlpasch  28983  hphl  28998  lnincplng  29010  plngrotlem2  29014  hypcgrlem1  29047  hypcgrlem2  29048  trgcopy  29052  trgcopyeulem  29053  cgracgr  29066  cgraswap  29068  cgrahl  29075  cgracol  29076  inagflat  29088  inaghl  29093  prlngref  29121  colinearalglem4  29164  axcontlem3  29221  edglnl  29398  clwlkclwwlklem2a  30254  clwwlknonmpo  30345  trlsegvdeg  30483  nfrgr2v  30528  frgrwopreg  30579  frgrreg  30650  ex-natded5.7  30667  ex-natded5.13  30671  ex-natded9.20  30673  ex-natded9.20-2  30674  f1ocnt  33053  linds2eq  33605  constrelextdg2  34049  submateqlem2  34110  measxun2  34512  measssd  34517  measiun  34520  meascnbl  34521  carsgclctun  34623  satfvsucsuc  35723  fmlasucdisj  35757  satfun  35769  satfv1fvfmla1  35781  2goelgoanfmla1  35782  outsideoftr  36487  lineunray  36505  weiunpo  36833  knoppndvlem6  36963  topdifinffinlem  37848  areacirclem4  38217  smprngopr  38558  tsbi1  38639  tsbi2  38640  lkrshpor  39738  2atmat0  40157  dochsnkrlem3  42102  dvrelog2b  42690  aks4d1p1  42700  aks6d1c2p2  42743  hashnexinjle  42753  unitscyglem2  42820  pell1234qrdich  43445  acongid  43559  acongtr  43562  acongrep  43564  acongeq  43567  jm2.23  43580  jm2.25  43583  jm2.27a  43589  kelac2lem  43648  mendvscafval  43770  fzunt1d  44040  rp-fakeimass  44095  frege106d  44338  clsk1indlem3  44626  nanorxor  44874  undif3VD  45449  refsum2cnlem1  45616  reclt0d  45961  limciccioolb  46196  limcicciooub  46210  wallispilem3  46640  fourierdlem35  46715  fourierdlem80  46759  fourierswlem  46803  fouriersw  46804  squeezedltsq  47463  dfatprc  47723  nltle2tri  47906  icceuelpartlem  48040  requad01  48242  even3prm2  48340  stgoldbwt  48397  clnbgrvtxel  48450  dfclnbgr6  48477  dfnbgr6  48478  dfsclnbgr6  48479  clnbgrgrim  48555  usgrexmpl2trifr  48658  gpgusgralem  48677  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem2  48693  gpg5nbgrvtx13starlem3  48694  gpg3nbgrvtx0  48697  gpg3nbgrvtx0ALT  48698  gpg3nbgrvtx1  48699  gpg5edgnedg  48751  smprngprmrng  48960  ztprmneprm  48979  altgsumbcALT  48985  zlmodzxznm  49129  zlmodzxzldeplem4  49135  reorelicc  49342  prelrrx2b  49346  rrx2plord1  49353  line2x  49386  itscnhlc0xyqsol  49397  itscnhlinecirc02plem1  49414  fvconst0ci  49521  upfval  49806