Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30431. (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  3799  rabsnifsb  4726  n0snor2el  4837  disjprg  5143  propeqop  5516  nf1oconst  7324  poxp  8151  xpord2indlem  8170  naddcllem  8712  unxpwdom2  9625  djuunxp  9958  sornom  10314  fin11a  10420  fin56  10430  fin1a2lem11  10447  axdc3lem2  10488  gchdomtri  10666  0tsk  10792  zmulcl  12663  nn0lt2  12678  nn01to3  12980  xrlttri  13177  xmulpnf1  13312  iccsplit  13521  elfznelfzo  13807  fvf1tp  13825  hashrabsn01  14408  hashsn01  14451  swrdnnn0nd  14690  zsum  15750  sumsplit  15800  zprod  15969  rpnnen2lem11  16256  lcmfunsnlem2lem1  16671  lcmfunsnlem2  16673  vdwlem6  17019  vdwlem10  17023  cshwshashlem1  17129  basprssdmsets  17257  mreexfidimd  17694  smndex1mgm  18932  sgrp2nmndlem5  18954  symg2bas  19424  psgnunilem1  19525  oppglsm  19674  gsummulgz  19975  prmgrpsimpgd  20148  srgbinomlem4  20246  dvrfval  20418  nrhmzr  20553  lringuplu  20560  cnsubrg  21462  marrepfval  22581  marepvfval  22586  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  fctop  23026  cctop  23028  pptbas  23030  metustto  24581  pmltpclem2  25497  dvne0  26064  taylplem2  26419  taylpfval  26420  dvntaylp0  26428  ang180lem3  26868  scvxcvx  27043  lgsdir2lem5  27387  sltres  27721  addsval  28009  mulsval  28149  mulsproplem13  28168  mulsproplem14  28169  zseo  28420  halfcut  28430  tgbtwnconn1  28597  tgbtwnconn2  28598  tgbtwnconn3  28599  legtrid  28613  hltr  28632  hlbtwn  28633  btwnhl1  28634  btwnhl2  28635  tglineneq  28666  ncolncol  28668  colmid  28710  footexALT  28740  footexlem2  28742  colperpexlem3  28754  colperpex  28755  mideulem2  28756  opphllem  28757  hlpasch  28778  hphl  28793  hypcgrlem1  28821  hypcgrlem2  28822  trgcopy  28826  trgcopyeulem  28827  cgracgr  28840  cgraswap  28842  cgrahl  28849  cgracol  28850  inagflat  28862  inaghl  28867  colinearalglem4  28938  axcontlem3  28995  edglnl  29174  clwlkclwwlklem2a  30026  clwwlknonmpo  30117  trlsegvdeg  30255  nfrgr2v  30300  frgrwopreg  30351  frgrreg  30422  ex-natded5.7  30439  ex-natded5.13  30443  ex-natded9.20  30445  ex-natded9.20-2  30446  padct  32736  f1ocnt  32809  linds2eq  33388  constrelextdg2  33751  submateqlem2  33768  measxun2  34190  measssd  34195  measiun  34198  meascnbl  34199  carsgclctun  34302  satfvsucsuc  35349  fmlasucdisj  35383  satfun  35395  satfv1fvfmla1  35407  2goelgoanfmla1  35408  outsideoftr  36110  lineunray  36128  weiunpo  36447  knoppndvlem6  36499  topdifinffinlem  37329  areacirclem4  37697  smprngopr  38038  tsbi1  38119  tsbi2  38120  lkrshpor  39088  2atmat0  39508  dochsnkrlem3  41453  dvrelog2b  42047  aks4d1p1  42057  aks6d1c2p2  42100  hashnexinjle  42110  unitscyglem2  42177  pell1234qrdich  42848  acongid  42963  acongtr  42966  acongrep  42968  acongeq  42971  jm2.23  42984  jm2.25  42987  jm2.27a  42993  kelac2lem  43052  mendvscafval  43174  fzunt1d  43446  rp-fakeimass  43501  frege106d  43744  clsk1indlem3  44032  nanorxor  44300  undif3VD  44879  refsum2cnlem1  44974  reclt0d  45336  limciccioolb  45576  limcicciooub  45592  wallispilem3  46022  fourierdlem35  46097  fourierdlem80  46141  fourierswlem  46185  fouriersw  46186  dfatprc  47079  nltle2tri  47262  icceuelpartlem  47359  requad01  47545  even3prm2  47643  stgoldbwt  47700  clnbgrvtxel  47753  dfclnbgr6  47779  dfnbgr6  47780  dfsclnbgr6  47781  clnbgrgrim  47839  usgrexmpl2trifr  47931  gpgusgralem  47945  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  ztprmneprm  48191  altgsumbcALT  48197  zlmodzxznm  48342  zlmodzxzldeplem4  48348  reorelicc  48559  prelrrx2b  48563  rrx2plord1  48570  line2x  48603  itscnhlc0xyqsol  48614  itscnhlinecirc02plem1  48631  fvconst0ci  48688