Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30385. (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  3746  rabsnifsb  4674  n0snor2el  4784  disjprg  5089  propeqop  5450  nf1oconst  7245  poxp  8064  xpord2indlem  8083  naddcllem  8597  unxpwdom2  9481  djuunxp  9821  sornom  10175  fin11a  10281  fin56  10291  fin1a2lem11  10308  axdc3lem2  10349  gchdomtri  10527  0tsk  10653  zmulcl  12527  nn0lt2  12542  nn01to3  12841  xrlttri  13040  xmulpnf1  13175  iccsplit  13387  elfznelfzo  13675  fvf1tp  13695  hashrabsn01  14282  hashsn01  14325  swrdnnn0nd  14566  zsum  15627  sumsplit  15677  zprod  15846  rpnnen2lem11  16135  lcmfunsnlem2lem1  16551  lcmfunsnlem2  16553  vdwlem6  16900  vdwlem10  16904  cshwshashlem1  17009  basprssdmsets  17134  mreexfidimd  17558  chnccat  18534  smndex1mgm  18817  sgrp2nmndlem5  18839  symg2bas  19307  psgnunilem1  19407  oppglsm  19556  gsummulgz  19857  prmgrpsimpgd  20030  srgbinomlem4  20149  dvrfval  20322  nrhmzr  20454  lringuplu  20461  cnsubrg  21366  marrepfval  22476  marepvfval  22481  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  fctop  22920  cctop  22922  pptbas  22924  metustto  24469  pmltpclem2  25378  dvne0  25944  taylplem2  26299  taylpfval  26300  dvntaylp0  26308  ang180lem3  26749  scvxcvx  26924  lgsdir2lem5  27268  sltres  27602  addsval  27906  mulsval  28049  mulsproplem13  28068  mulsproplem14  28069  onscutlt  28202  n0sfincut  28283  zseo  28346  halfcut  28379  zs12zodd  28393  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  28889  axcontlem3  28946  edglnl  29123  clwlkclwwlklem2a  29980  clwwlknonmpo  30071  trlsegvdeg  30209  nfrgr2v  30254  frgrwopreg  30305  frgrreg  30376  ex-natded5.7  30393  ex-natded5.13  30397  ex-natded9.20  30399  ex-natded9.20-2  30400  padct  32705  f1ocnt  32787  linds2eq  33353  constrelextdg2  33781  submateqlem2  33842  measxun2  34244  measssd  34249  measiun  34252  meascnbl  34253  carsgclctun  34355  satfvsucsuc  35430  fmlasucdisj  35464  satfun  35476  satfv1fvfmla1  35488  2goelgoanfmla1  35489  outsideoftr  36194  lineunray  36212  weiunpo  36530  knoppndvlem6  36582  topdifinffinlem  37412  areacirclem4  37772  smprngopr  38113  tsbi1  38194  tsbi2  38195  lkrshpor  39227  2atmat0  39646  dochsnkrlem3  41591  dvrelog2b  42180  aks4d1p1  42190  aks6d1c2p2  42233  hashnexinjle  42243  unitscyglem2  42310  pell1234qrdich  42979  acongid  43093  acongtr  43096  acongrep  43098  acongeq  43101  jm2.23  43114  jm2.25  43117  jm2.27a  43123  kelac2lem  43182  mendvscafval  43304  fzunt1d  43575  rp-fakeimass  43630  frege106d  43873  clsk1indlem3  44161  nanorxor  44423  undif3VD  44999  refsum2cnlem1  45159  reclt0d  45510  limciccioolb  45746  limcicciooub  45760  wallispilem3  46190  fourierdlem35  46265  fourierdlem80  46309  fourierswlem  46353  fouriersw  46354  squeezedltsq  47011  dfatprc  47255  nltle2tri  47438  icceuelpartlem  47560  requad01  47746  even3prm2  47844  stgoldbwt  47901  clnbgrvtxel  47954  dfclnbgr6  47981  dfnbgr6  47982  dfsclnbgr6  47983  clnbgrgrim  48059  usgrexmpl2trifr  48162  gpgusgralem  48181  gpg5nbgrvtx03starlem1  48193  gpg5nbgrvtx03starlem2  48194  gpg5nbgrvtx03starlem3  48195  gpg5nbgrvtx13starlem1  48196  gpg5nbgrvtx13starlem2  48197  gpg5nbgrvtx13starlem3  48198  gpg3nbgrvtx0  48201  gpg3nbgrvtx0ALT  48202  gpg3nbgrvtx1  48203  gpg5edgnedg  48255  ztprmneprm  48472  altgsumbcALT  48478  zlmodzxznm  48623  zlmodzxzldeplem4  48629  reorelicc  48836  prelrrx2b  48840  rrx2plord1  48847  line2x  48880  itscnhlc0xyqsol  48891  itscnhlinecirc02plem1  48908  fvconst0ci  49016  upfval  49302