Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30339. (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  3765  rabsnifsb  4689  n0snor2el  4800  disjprg  5106  propeqop  5470  nf1oconst  7283  poxp  8110  xpord2indlem  8129  naddcllem  8643  unxpwdom2  9548  djuunxp  9881  sornom  10237  fin11a  10343  fin56  10353  fin1a2lem11  10370  axdc3lem2  10411  gchdomtri  10589  0tsk  10715  zmulcl  12589  nn0lt2  12604  nn01to3  12907  xrlttri  13106  xmulpnf1  13241  iccsplit  13453  elfznelfzo  13740  fvf1tp  13758  hashrabsn01  14345  hashsn01  14388  swrdnnn0nd  14628  zsum  15691  sumsplit  15741  zprod  15910  rpnnen2lem11  16199  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  vdwlem6  16964  vdwlem10  16968  cshwshashlem1  17073  basprssdmsets  17198  mreexfidimd  17618  smndex1mgm  18841  sgrp2nmndlem5  18863  symg2bas  19330  psgnunilem1  19430  oppglsm  19579  gsummulgz  19880  prmgrpsimpgd  20053  srgbinomlem4  20145  dvrfval  20318  nrhmzr  20453  lringuplu  20460  cnsubrg  21351  marrepfval  22454  marepvfval  22459  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  fctop  22898  cctop  22900  pptbas  22902  metustto  24448  pmltpclem2  25357  dvne0  25923  taylplem2  26278  taylpfval  26279  dvntaylp0  26287  ang180lem3  26728  scvxcvx  26903  lgsdir2lem5  27247  sltres  27581  addsval  27876  mulsval  28019  mulsproplem13  28038  mulsproplem14  28039  onscutlt  28172  n0sfincut  28253  zseo  28315  halfcut  28340  tgbtwnconn1  28509  tgbtwnconn2  28510  tgbtwnconn3  28511  legtrid  28525  hltr  28544  hlbtwn  28545  btwnhl1  28546  btwnhl2  28547  tglineneq  28578  ncolncol  28580  colmid  28622  footexALT  28652  footexlem2  28654  colperpexlem3  28666  colperpex  28667  mideulem2  28668  opphllem  28669  hlpasch  28690  hphl  28705  hypcgrlem1  28733  hypcgrlem2  28734  trgcopy  28738  trgcopyeulem  28739  cgracgr  28752  cgraswap  28754  cgrahl  28761  cgracol  28762  inagflat  28774  inaghl  28779  colinearalglem4  28843  axcontlem3  28900  edglnl  29077  clwlkclwwlklem2a  29934  clwwlknonmpo  30025  trlsegvdeg  30163  nfrgr2v  30208  frgrwopreg  30259  frgrreg  30330  ex-natded5.7  30347  ex-natded5.13  30351  ex-natded9.20  30353  ex-natded9.20-2  30354  padct  32650  f1ocnt  32732  linds2eq  33359  constrelextdg2  33744  submateqlem2  33805  measxun2  34207  measssd  34212  measiun  34215  meascnbl  34216  carsgclctun  34319  satfvsucsuc  35359  fmlasucdisj  35393  satfun  35405  satfv1fvfmla1  35417  2goelgoanfmla1  35418  outsideoftr  36124  lineunray  36142  weiunpo  36460  knoppndvlem6  36512  topdifinffinlem  37342  areacirclem4  37712  smprngopr  38053  tsbi1  38134  tsbi2  38135  lkrshpor  39107  2atmat0  39527  dochsnkrlem3  41472  dvrelog2b  42061  aks4d1p1  42071  aks6d1c2p2  42114  hashnexinjle  42124  unitscyglem2  42191  pell1234qrdich  42856  acongid  42971  acongtr  42974  acongrep  42976  acongeq  42979  jm2.23  42992  jm2.25  42995  jm2.27a  43001  kelac2lem  43060  mendvscafval  43182  fzunt1d  43453  rp-fakeimass  43508  frege106d  43751  clsk1indlem3  44039  nanorxor  44301  undif3VD  44878  refsum2cnlem1  45038  reclt0d  45390  limciccioolb  45626  limcicciooub  45642  wallispilem3  46072  fourierdlem35  46147  fourierdlem80  46191  fourierswlem  46235  fouriersw  46236  squeezedltsq  46894  dfatprc  47135  nltle2tri  47318  icceuelpartlem  47440  requad01  47626  even3prm2  47724  stgoldbwt  47781  clnbgrvtxel  47834  dfclnbgr6  47860  dfnbgr6  47861  dfsclnbgr6  47862  clnbgrgrim  47938  usgrexmpl2trifr  48032  gpgusgralem  48051  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  ztprmneprm  48339  altgsumbcALT  48345  zlmodzxznm  48490  zlmodzxzldeplem4  48496  reorelicc  48703  prelrrx2b  48707  rrx2plord1  48714  line2x  48747  itscnhlc0xyqsol  48758  itscnhlinecirc02plem1  48775  fvconst0ci  48883  upfval  49169