Theorem orcd 887

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 31010. (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  3747  rabsnifsb  4679  n0snor2el  4787  disjprg  5098  propeqop  5478  nf1oconst  7314  poxp  8143  xpord2indlem  8167  naddcllem  8689  unxpwdom2  9586  djuunxp  10006  sornom  10359  fin11a  10465  fin56  10475  fin1a2lem11  10492  axdc3lem2  10533  gchdomtri  10718  0tsk  10844  zmulcl  12749  nn0lt2  12766  nn01to3  13072  xrlttri  13272  xmulpnf1  13408  iccsplit  13620  elfznelfzo  13912  fvf1tp  13933  hashrabsn01  14521  hashsn01  14565  swrdnnn0nd  14811  zsum  15890  sumsplit  15940  zprod  16110  rpnnen2lem11  16398  lcmfunsnlem2lem1  16819  lcmfunsnlem2  16821  vdwlem6  17170  vdwlem10  17174  cshwshashlem1  17279  basprssdmsets  17405  mreexfidimd  17830  chnccat  18806  smndex1mgm  19112  sgrp2nmndlem5  19134  symg2bas  19613  psgnunilem1  19713  oppglsm  19862  gsummulgz  20163  prmgrpsimpgd  20336  srgbinomlem4  20461  dvrfval  20638  nrhmzr  20795  lringuplu  20802  isfieldidl  21546  cnsubrg  21739  marrepfval  22881  marepvfval  22886  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  fctop  23328  cctop  23330  pptbas  23332  metustto  24878  pmltpclem2  25776  dvne0  26337  taylplem2  26697  taylpfval  26698  dvntaylp0  26705  ang180lem3  27145  scvxcvx  27319  lgsdir2lem5  27662  fltoprmlem1  27999  ltsres  28025  addsval  28354  mulsval  28501  mulsproplem13  28520  mulsproplem14  28521  oncutlt  28656  n0fincut  28747  zseo  28814  halfcut  28850  z12zsodd  28874  tgbtwnconn1  29044  tgbtwnconn2  29045  tgbtwnconn3  29046  legtrid  29060  hltr  29082  hlbtwn  29083  btwnhl1  29084  btwnhl2  29085  tglineneq  29119  ncolncol  29121  colmid  29166  symquadprlnglem  29171  footexALT  29199  footexlem2  29201  colperpexlem3  29214  colperpex  29215  mideulem2  29216  opphllem  29217  hlpasch  29240  hphl  29255  hlopp  29256  lnincplng  29268  plngrotlem2  29272  symquadmid  29310  hypcgrlem1  29311  hypcgrlem2  29312  trgcopy  29317  trgcopyeulem  29318  cgracgr  29331  cgraswap  29333  cgrahl  29341  cgracol  29342  ragcgra  29349  cgrarag  29350  inagflat  29365  inaghl  29370  angmgmaddeu1  29385  angmgmaddcpbl  29396  prlngref  29424  symquadprlng  29446  colinearalglem4  29493  axcontlem3  29550  edglnl  29727  clwlkclwwlklem2a  30595  clwwlknonmpo  30686  trlsegvdeg  30834  nfrgr2v  30879  frgrwopreg  30930  frgrreg  31001  ex-natded5.7  31018  ex-natded5.13  31022  ex-natded9.20  31024  ex-natded9.20-2  31025  inagcgrasubbtwn  33056  inagcgrabtwn  33057  cgrgptxfr  33059  cgrainag  33066  tgaasncol  33086  f1ocnt  33439  linds2eq  33983  constrelextdg2  34426  submateqlem2  34487  measxun2  34890  measssd  34895  measiun  34898  meascnbl  34899  carsgclctun  35000  onprcf1of1ord  35975  satfvsucsuc  36217  fmlasucdisj  36251  satfun  36263  satfv1fvfmla1  36275  2goelgoanfmla1  36276  outsideoftr  36987  lineunray  37005  weiunpo  37346  knoppndvlem6  37476  topdifinffinlem  38364  areacirclem4  38723  negprop  38737  impprop  38738  smprngopr  39080  tsbi1  39159  tsbi2  39160  lkrshpor  40258  2atmat0  40677  dochsnkrlem3  42622  dvrelog2b  43210  aks4d1p1  43220  aks6d1c2p2  43263  hashnexinjle  43273  unitscyglem2  43340  pell1234qrdich  43962  acongid  44076  acongtr  44079  acongrep  44081  acongeq  44084  jm2.23  44097  jm2.25  44100  jm2.27a  44106  kelac2lem  44160  mendvscafval  44282  fzunt1d  44552  rp-fakeimass  44607  frege106d  44849  clsk1indlem3  45137  nanorxor  45383  undif3VD  45958  refsum2cnlem1  46148  reclt0d  46492  limciccioolb  46727  limcicciooub  46741  wallispilem3  47171  fourierdlem35  47246  fourierdlem80  47290  fourierswlem  47334  fouriersw  47335  dfatprc  48294  nltle2tri  48477  icceuelpartlem  48611  requad01  48813  even3prm2  48911  stgoldbwt  48968  clnbgrvtxel  49021  dfclnbgr6  49048  dfnbgr6  49049  dfsclnbgr6  49050  clnbgrgrim  49126  usgrexmpl2trifr  49229  gpgusgralem  49248  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg3nbgrvtx0  49268  gpg3nbgrvtx0ALT  49269  gpg3nbgrvtx1  49270  gpg5edgnedg  49322  smprngprmrng  49530  ztprmneprm  49553  altgsumbcALT  49559  zlmodzxznm  49703  zlmodzxzldeplem4  49709  reorelicc  49916  rrx2plord1  49928  itscnhlc0xyqsol  49971  itscnhlinecirc02plem1  49988  fvconst0ci  50099  upfval  50386  parhomcl2  50839