Theorem orcd 887

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 31037. (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  3751  rabsnifsb  4683  n0snor2el  4791  disjprg  5102  propeqop  5484  nf1oconst  7339  poxp  8170  xpord2indlem  8194  naddcllem  8716  unxpwdom2  9612  djuunxp  10032  sornom  10385  fin11a  10491  fin56  10501  fin1a2lem11  10518  axdc3lem2  10559  gchdomtri  10744  0tsk  10870  zmulcl  12775  nn0lt2  12792  nn01to3  13098  xrlttri  13298  xmulpnf1  13434  iccsplit  13646  elfznelfzo  13938  fvf1tp  13959  hashrabsn01  14547  hashsn01  14591  swrdnnn0nd  14837  zsum  15916  sumsplit  15966  zprod  16136  rpnnen2lem11  16424  lcmfunsnlem2lem1  16845  lcmfunsnlem2  16847  vdwlem6  17196  vdwlem10  17200  cshwshashlem1  17305  basprssdmsets  17431  mreexfidimd  17856  chnccat  18832  smndex1mgm  19138  sgrp2nmndlem5  19160  symg2bas  19640  psgnunilem1  19740  oppglsm  19889  gsummulgz  20190  prmgrpsimpgd  20363  srgbinomlem4  20488  dvrfval  20665  nrhmzr  20822  lringuplu  20829  isfieldidl  21573  cnsubrg  21766  marrepfval  22908  marepvfval  22913  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  fctop  23355  cctop  23357  pptbas  23359  metustto  24905  pmltpclem2  25803  dvne0  26364  taylplem2  26724  taylpfval  26725  dvntaylp0  26732  ang180lem3  27172  scvxcvx  27346  lgsdir2lem5  27689  fltoprmlem1  28026  ltsres  28052  addsval  28381  mulsval  28528  mulsproplem13  28547  mulsproplem14  28548  oncutlt  28683  n0fincut  28774  zseo  28841  halfcut  28877  z12zsodd  28901  tgbtwnconn1  29071  tgbtwnconn2  29072  tgbtwnconn3  29073  legtrid  29087  hltr  29109  hlbtwn  29110  btwnhl1  29111  btwnhl2  29112  tglineneq  29146  ncolncol  29148  colmid  29193  symquadprlnglem  29198  footexALT  29226  footexlem2  29228  colperpexlem3  29241  colperpex  29242  mideulem2  29243  opphllem  29244  hlpasch  29267  hphl  29282  hlopp  29283  lnincplng  29295  plngrotlem2  29299  symquadmid  29337  hypcgrlem1  29338  hypcgrlem2  29339  trgcopy  29344  trgcopyeulem  29345  cgracgr  29358  cgraswap  29360  cgrahl  29368  cgracol  29369  ragcgra  29376  cgrarag  29377  inagflat  29392  inaghl  29397  angmgmaddeu1  29412  angmgmaddcpbl  29423  prlngref  29451  symquadprlng  29473  colinearalglem4  29520  axcontlem3  29577  edglnl  29754  clwlkclwwlklem2a  30622  clwwlknonmpo  30713  trlsegvdeg  30861  nfrgr2v  30906  frgrwopreg  30957  frgrreg  31028  ex-natded5.7  31045  ex-natded5.13  31049  ex-natded9.20  31051  ex-natded9.20-2  31052  inagcgrasubbtwn  33083  inagcgrabtwn  33084  cgrgptxfr  33086  cgrainag  33093  tgaasncol  33113  f1ocnt  33465  fldedom  33937  linds2eq  34020  constrelextdg2  34462  submateqlem2  34523  measxun2  34926  measssd  34931  measiun  34934  meascnbl  34935  carsgclctun  35036  onprcf1of1ord  36068  satfvsucsuc  36310  fmlasucdisj  36344  satfun  36356  satfv1fvfmla1  36368  2goelgoanfmla1  36369  outsideoftr  37085  lineunray  37103  weiunpo  37444  knoppndvlem6  37574  topdifinffinlem  38475  areacirclem4  38834  negprop  38848  impprop  38849  smprngopr  39189  tsbi1  39268  tsbi2  39269  lkrshpor  40367  2atmat0  40786  dochsnkrlem3  42731  dvrelog2b  43319  aks4d1p1  43329  aks6d1c2p2  43372  hashnexinjle  43382  unitscyglem2  43449  pell1234qrdich  44072  acongid  44186  acongtr  44189  acongrep  44191  acongeq  44194  jm2.23  44207  jm2.25  44210  jm2.27a  44216  kelac2lem  44270  mendvscafval  44391  fzunt1d  44661  rp-fakeimass  44716  frege106d  44958  clsk1indlem3  45246  nanorxor  45492  undif3VD  46066  refsum2cnlem1  46270  reclt0d  46613  limciccioolb  46848  limcicciooub  46862  wallispilem3  47292  fourierdlem35  47367  fourierdlem80  47411  fourierswlem  47455  fouriersw  47456  dfatprc  48415  nltle2tri  48598  icceuelpartlem  48732  requad01  48934  even3prm2  49032  stgoldbwt  49089  clnbgrvtxel  49142  dfclnbgr6  49169  dfnbgr6  49170  dfsclnbgr6  49171  clnbgrgrim  49247  usgrexmpl2trifr  49350  gpgusgralem  49369  gpg5nbgrvtx03starlem1  49381  gpg5nbgrvtx03starlem2  49382  gpg5nbgrvtx03starlem3  49383  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem2  49385  gpg5nbgrvtx13starlem3  49386  gpg3nbgrvtx0  49389  gpg3nbgrvtx0ALT  49390  gpg3nbgrvtx1  49391  gpg5edgnedg  49443  smprngprmrng  49651  ztprmneprm  49674  altgsumbcALT  49680  zlmodzxznm  49824  zlmodzxzldeplem4  49830  reorelicc  50037  rrx2plord1  50049  itscnhlc0xyqsol  50092  itscnhlinecirc02plem1  50109  fvconst0ci  50220  upfval  50507  parhomcl2  50960