Theorem orcd 884

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  olcd  885  pm2.47  894  orim12i  919  animorl  990  animorrl  993  cases2ALT  1059  sbc2or  3753  rabsnifsb  4680  n0snor2el  4790  disjprg  5095  propeqop  5475  nf1oconst  7285  poxp  8103  xpord2indlem  8122  naddcllem  8641  unxpwdom2  9533  djuunxp  9876  sornom  10231  fin11a  10337  fin56  10347  fin1a2lem11  10364  axdc3lem2  10405  gchdomtri  10584  0tsk  10710  zmulcl  12617  nn0lt2  12633  nn01to3  12939  xrlttri  13138  xmulpnf1  13274  iccsplit  13486  elfznelfzo  13776  fvf1tp  13796  hashrabsn01  14383  hashsn01  14426  swrdnnn0nd  14667  zsum  15728  sumsplit  15778  zprod  15950  rpnnen2lem11  16239  lcmfunsnlem2lem1  16655  lcmfunsnlem2  16657  vdwlem6  17005  vdwlem10  17009  cshwshashlem1  17114  basprssdmsets  17240  mreexfidimd  17665  chnccat  18641  smndex1mgm  18927  sgrp2nmndlem5  18949  symg2bas  19416  psgnunilem1  19516  oppglsm  19665  gsummulgz  19966  prmgrpsimpgd  20139  srgbinomlem4  20258  dvrfval  20430  nrhmzr  20566  lringuplu  20573  cnsubrg  21459  marrepfval  22600  marepvfval  22605  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  fctop  23044  cctop  23046  pptbas  23048  metustto  24593  pmltpclem2  25491  dvne0  26053  taylplem2  26404  taylpfval  26405  dvntaylp0  26412  ang180lem3  26853  scvxcvx  27027  lgsdir2lem5  27370  ltsres  27703  addsval  28032  mulsval  28179  mulsproplem13  28198  mulsproplem14  28199  oncutlt  28334  n0fincut  28425  zseo  28492  halfcut  28528  z12zsodd  28552  tgbtwnconn1  28721  tgbtwnconn2  28722  tgbtwnconn3  28723  legtrid  28737  hltr  28756  hlbtwn  28757  btwnhl1  28758  btwnhl2  28759  tglineneq  28790  ncolncol  28792  colmid  28834  footexALT  28864  footexlem2  28866  colperpexlem3  28878  colperpex  28879  mideulem2  28880  opphllem  28881  hlpasch  28902  hphl  28917  hypcgrlem1  28945  hypcgrlem2  28946  trgcopy  28950  trgcopyeulem  28951  cgracgr  28964  cgraswap  28966  cgrahl  28973  cgracol  28974  inagflat  28986  inaghl  28991  colinearalglem4  29056  axcontlem3  29113  edglnl  29290  clwlkclwwlklem2a  30146  clwwlknonmpo  30237  trlsegvdeg  30375  nfrgr2v  30420  frgrwopreg  30471  frgrreg  30542  ex-natded5.7  30559  ex-natded5.13  30563  ex-natded9.20  30565  ex-natded9.20-2  30566  f1ocnt  32952  linds2eq  33528  constrelextdg2  34005  submateqlem2  34066  measxun2  34468  measssd  34473  measiun  34476  meascnbl  34477  carsgclctun  34579  satfvsucsuc  35679  fmlasucdisj  35713  satfun  35725  satfv1fvfmla1  35737  2goelgoanfmla1  35738  outsideoftr  36443  lineunray  36461  weiunpo  36789  knoppndvlem6  36919  topdifinffinlem  37805  areacirclem4  38174  smprngopr  38515  tsbi1  38596  tsbi2  38597  lkrshpor  39695  2atmat0  40114  dochsnkrlem3  42059  dvrelog2b  42647  aks4d1p1  42657  aks6d1c2p2  42700  hashnexinjle  42710  unitscyglem2  42777  pell1234qrdich  43402  acongid  43516  acongtr  43519  acongrep  43521  acongeq  43524  jm2.23  43537  jm2.25  43540  jm2.27a  43546  kelac2lem  43605  mendvscafval  43727  fzunt1d  43997  rp-fakeimass  44052  frege106d  44295  clsk1indlem3  44583  nanorxor  44845  undif3VD  45421  refsum2cnlem1  45581  reclt0d  45926  limciccioolb  46161  limcicciooub  46175  wallispilem3  46605  fourierdlem35  46680  fourierdlem80  46724  fourierswlem  46768  fouriersw  46769  squeezedltsq  47428  dfatprc  47688  nltle2tri  47871  icceuelpartlem  48005  requad01  48207  even3prm2  48305  stgoldbwt  48362  clnbgrvtxel  48415  dfclnbgr6  48442  dfnbgr6  48443  dfsclnbgr6  48444  clnbgrgrim  48520  usgrexmpl2trifr  48623  gpgusgralem  48642  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpg3nbgrvtx0  48662  gpg3nbgrvtx0ALT  48663  gpg3nbgrvtx1  48664  gpg5edgnedg  48716  ztprmneprm  48933  altgsumbcALT  48939  zlmodzxznm  49083  zlmodzxzldeplem4  49089  reorelicc  49296  prelrrx2b  49300  rrx2plord1  49307  line2x  49340  itscnhlc0xyqsol  49351  itscnhlinecirc02plem1  49368  fvconst0ci  49476  upfval  49761