Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30332. (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  3762  rabsnifsb  4686  n0snor2el  4797  disjprg  5103  propeqop  5467  nf1oconst  7280  poxp  8107  xpord2indlem  8126  naddcllem  8640  unxpwdom2  9541  djuunxp  9874  sornom  10230  fin11a  10336  fin56  10346  fin1a2lem11  10363  axdc3lem2  10404  gchdomtri  10582  0tsk  10708  zmulcl  12582  nn0lt2  12597  nn01to3  12900  xrlttri  13099  xmulpnf1  13234  iccsplit  13446  elfznelfzo  13733  fvf1tp  13751  hashrabsn01  14338  hashsn01  14381  swrdnnn0nd  14621  zsum  15684  sumsplit  15734  zprod  15903  rpnnen2lem11  16192  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  vdwlem6  16957  vdwlem10  16961  cshwshashlem1  17066  basprssdmsets  17191  mreexfidimd  17611  smndex1mgm  18834  sgrp2nmndlem5  18856  symg2bas  19323  psgnunilem1  19423  oppglsm  19572  gsummulgz  19873  prmgrpsimpgd  20046  srgbinomlem4  20138  dvrfval  20311  nrhmzr  20446  lringuplu  20453  cnsubrg  21344  marrepfval  22447  marepvfval  22452  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  fctop  22891  cctop  22893  pptbas  22895  metustto  24441  pmltpclem2  25350  dvne0  25916  taylplem2  26271  taylpfval  26272  dvntaylp0  26280  ang180lem3  26721  scvxcvx  26896  lgsdir2lem5  27240  sltres  27574  addsval  27869  mulsval  28012  mulsproplem13  28031  mulsproplem14  28032  onscutlt  28165  n0sfincut  28246  zseo  28308  halfcut  28333  tgbtwnconn1  28502  tgbtwnconn2  28503  tgbtwnconn3  28504  legtrid  28518  hltr  28537  hlbtwn  28538  btwnhl1  28539  btwnhl2  28540  tglineneq  28571  ncolncol  28573  colmid  28615  footexALT  28645  footexlem2  28647  colperpexlem3  28659  colperpex  28660  mideulem2  28661  opphllem  28662  hlpasch  28683  hphl  28698  hypcgrlem1  28726  hypcgrlem2  28727  trgcopy  28731  trgcopyeulem  28732  cgracgr  28745  cgraswap  28747  cgrahl  28754  cgracol  28755  inagflat  28767  inaghl  28772  colinearalglem4  28836  axcontlem3  28893  edglnl  29070  clwlkclwwlklem2a  29927  clwwlknonmpo  30018  trlsegvdeg  30156  nfrgr2v  30201  frgrwopreg  30252  frgrreg  30323  ex-natded5.7  30340  ex-natded5.13  30344  ex-natded9.20  30346  ex-natded9.20-2  30347  padct  32643  f1ocnt  32725  linds2eq  33352  constrelextdg2  33737  submateqlem2  33798  measxun2  34200  measssd  34205  measiun  34208  meascnbl  34209  carsgclctun  34312  satfvsucsuc  35352  fmlasucdisj  35386  satfun  35398  satfv1fvfmla1  35410  2goelgoanfmla1  35411  outsideoftr  36117  lineunray  36135  weiunpo  36453  knoppndvlem6  36505  topdifinffinlem  37335  areacirclem4  37705  smprngopr  38046  tsbi1  38127  tsbi2  38128  lkrshpor  39100  2atmat0  39520  dochsnkrlem3  41465  dvrelog2b  42054  aks4d1p1  42064  aks6d1c2p2  42107  hashnexinjle  42117  unitscyglem2  42184  pell1234qrdich  42849  acongid  42964  acongtr  42967  acongrep  42969  acongeq  42972  jm2.23  42985  jm2.25  42988  jm2.27a  42994  kelac2lem  43053  mendvscafval  43175  fzunt1d  43446  rp-fakeimass  43501  frege106d  43744  clsk1indlem3  44032  nanorxor  44294  undif3VD  44871  refsum2cnlem1  45031  reclt0d  45383  limciccioolb  45619  limcicciooub  45635  wallispilem3  46065  fourierdlem35  46140  fourierdlem80  46184  fourierswlem  46228  fouriersw  46229  squeezedltsq  46887  dfatprc  47131  nltle2tri  47314  icceuelpartlem  47436  requad01  47622  even3prm2  47720  stgoldbwt  47777  clnbgrvtxel  47830  dfclnbgr6  47856  dfnbgr6  47857  dfsclnbgr6  47858  clnbgrgrim  47934  usgrexmpl2trifr  48028  gpgusgralem  48047  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  ztprmneprm  48335  altgsumbcALT  48341  zlmodzxznm  48486  zlmodzxzldeplem4  48492  reorelicc  48699  prelrrx2b  48703  rrx2plord1  48710  line2x  48743  itscnhlc0xyqsol  48754  itscnhlinecirc02plem1  48771  fvconst0ci  48879  upfval  49165