Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 28486. (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 210  df-or 848

This theorem is referenced by:  olcd  874  pm2.47  884  orim12i  909  animorl  978  animorrl  981  cases2ALT  1049  sbc2or  3703  rabsnifsb  4638  n0snor2el  4744  disjprgw  5048  disjprg  5049  propeqop  5390  nf1oconst  7115  poxp  7895  unxpwdom2  9204  djuunxp  9537  sornom  9891  fin11a  9997  fin56  10007  fin1a2lem11  10024  axdc3lem2  10065  gchdomtri  10243  0tsk  10369  zmulcl  12226  nn0lt2  12240  nn01to3  12537  xrlttri  12729  xmulpnf1  12864  iccsplit  13073  elfznelfzo  13347  hashrabsn01  13940  hashsn01  13983  swrdnnn0nd  14221  zsum  15282  sumsplit  15332  zprod  15499  rpnnen2lem11  15785  lcmfunsnlem2lem1  16195  lcmfunsnlem2  16197  vdwlem6  16539  vdwlem10  16543  cshwshashlem1  16649  basprssdmsets  16772  mreexfidimd  17153  smndex1mgm  18334  sgrp2nmndlem5  18356  symg2bas  18785  psgnunilem1  18885  oppglsm  19031  gsummulgz  19328  prmgrpsimpgd  19501  srgbinomlem4  19558  dvrfval  19702  cnsubrg  20423  marrepfval  21457  marepvfval  21462  chfacfscmulgsum  21757  chfacfpmmulgsum  21761  fctop  21901  cctop  21903  pptbas  21905  metustto  23451  pmltpclem2  24346  dvne0  24908  taylplem2  25256  taylpfval  25257  dvntaylp0  25264  ang180lem3  25694  scvxcvx  25868  lgsdir2lem5  26210  tgbtwnconn1  26666  tgbtwnconn2  26667  tgbtwnconn3  26668  legtrid  26682  hltr  26701  hlbtwn  26702  btwnhl1  26703  btwnhl2  26704  tglineneq  26735  ncolncol  26737  colmid  26779  footexALT  26809  footexlem2  26811  colperpexlem3  26823  colperpex  26824  mideulem2  26825  opphllem  26826  hlpasch  26847  hphl  26862  hypcgrlem1  26890  hypcgrlem2  26891  trgcopy  26895  trgcopyeulem  26896  cgracgr  26909  cgraswap  26911  cgrahl  26918  cgracol  26919  inagflat  26931  inaghl  26936  colinearalglem4  27000  axcontlem3  27057  edglnl  27234  clwlkclwwlklem2a  28081  clwwlknonmpo  28172  trlsegvdeg  28310  nfrgr2v  28355  frgrwopreg  28406  frgrreg  28477  ex-natded5.7  28494  ex-natded5.13  28498  ex-natded9.20  28500  ex-natded9.20-2  28501  padct  30774  f1ocnt  30843  linds2eq  31289  submateqlem2  31472  measxun2  31890  measssd  31895  measiun  31898  meascnbl  31899  carsgclctun  32000  satfvsucsuc  33040  fmlasucdisj  33074  satfun  33086  satfv1fvfmla1  33098  2goelgoanfmla1  33099  xpord2ind  33531  naddcllem  33568  sltres  33602  addsval  33863  outsideoftr  34168  lineunray  34186  knoppndvlem6  34434  topdifinffinlem  35255  areacirclem4  35605  smprngopr  35947  tsbi1  36028  tsbi2  36029  lkrshpor  36858  2atmat0  37277  dochsnkrlem3  39222  dvrelog2b  39807  aks4d1p1  39817  pell1234qrdich  40386  acongid  40500  acongtr  40503  acongrep  40505  acongeq  40508  jm2.23  40521  jm2.25  40524  jm2.27a  40530  kelac2lem  40592  mendvscafval  40718  rp-fakeimass  40804  frege106d  41040  clsk1indlem3  41330  nanorxor  41596  undif3VD  42175  refsum2cnlem1  42253  reclt0d  42599  limciccioolb  42837  limcicciooub  42853  wallispilem3  43283  fourierdlem35  43358  fourierdlem80  43402  fourierswlem  43446  fouriersw  43447  dfatprc  44294  nltle2tri  44478  icceuelpartlem  44560  requad01  44746  even3prm2  44844  stgoldbwt  44901  isomuspgrlem1  44952  nrhmzr  45104  ztprmneprm  45356  altgsumbcALT  45362  zlmodzxznm  45511  zlmodzxzldeplem4  45517  reorelicc  45729  prelrrx2b  45733  rrx2plord1  45740  line2x  45773  itscnhlc0xyqsol  45784  itscnhlinecirc02plem1  45801  fvconst0ci  45859