Theorem orcd 872

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30435. (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 866	. 2 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:   → wi 4   ∨ wo 846

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 847

This theorem is referenced by:  olcd  873  pm2.47  882  orim12i  907  animorl  978  animorrl  981  cases2ALT  1049  sbc2or  3813  rabsnifsb  4747  n0snor2el  4858  disjprg  5162  propeqop  5526  nf1oconst  7341  poxp  8169  xpord2indlem  8188  naddcllem  8732  unxpwdom2  9657  djuunxp  9990  sornom  10346  fin11a  10452  fin56  10462  fin1a2lem11  10479  axdc3lem2  10520  gchdomtri  10698  0tsk  10824  zmulcl  12692  nn0lt2  12706  nn01to3  13006  xrlttri  13201  xmulpnf1  13336  iccsplit  13545  elfznelfzo  13822  fvf1tp  13840  hashrabsn01  14422  hashsn01  14465  swrdnnn0nd  14704  zsum  15766  sumsplit  15816  zprod  15985  rpnnen2lem11  16272  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  vdwlem6  17033  vdwlem10  17037  cshwshashlem1  17143  basprssdmsets  17271  mreexfidimd  17708  smndex1mgm  18942  sgrp2nmndlem5  18964  symg2bas  19434  psgnunilem1  19535  oppglsm  19684  gsummulgz  19985  prmgrpsimpgd  20158  srgbinomlem4  20256  dvrfval  20428  nrhmzr  20563  lringuplu  20570  cnsubrg  21468  marrepfval  22587  marepvfval  22592  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  fctop  23032  cctop  23034  pptbas  23036  metustto  24587  pmltpclem2  25503  dvne0  26070  taylplem2  26423  taylpfval  26424  dvntaylp0  26432  ang180lem3  26872  scvxcvx  27047  lgsdir2lem5  27391  sltres  27725  addsval  28013  mulsval  28153  mulsproplem13  28172  mulsproplem14  28173  zseo  28424  halfcut  28434  tgbtwnconn1  28601  tgbtwnconn2  28602  tgbtwnconn3  28603  legtrid  28617  hltr  28636  hlbtwn  28637  btwnhl1  28638  btwnhl2  28639  tglineneq  28670  ncolncol  28672  colmid  28714  footexALT  28744  footexlem2  28746  colperpexlem3  28758  colperpex  28759  mideulem2  28760  opphllem  28761  hlpasch  28782  hphl  28797  hypcgrlem1  28825  hypcgrlem2  28826  trgcopy  28830  trgcopyeulem  28831  cgracgr  28844  cgraswap  28846  cgrahl  28853  cgracol  28854  inagflat  28866  inaghl  28871  colinearalglem4  28942  axcontlem3  28999  edglnl  29178  clwlkclwwlklem2a  30030  clwwlknonmpo  30121  trlsegvdeg  30259  nfrgr2v  30304  frgrwopreg  30355  frgrreg  30426  ex-natded5.7  30443  ex-natded5.13  30447  ex-natded9.20  30449  ex-natded9.20-2  30450  padct  32733  f1ocnt  32807  linds2eq  33374  constrelextdg2  33737  submateqlem2  33754  measxun2  34174  measssd  34179  measiun  34182  meascnbl  34183  carsgclctun  34286  satfvsucsuc  35333  fmlasucdisj  35367  satfun  35379  satfv1fvfmla1  35391  2goelgoanfmla1  35392  outsideoftr  36093  lineunray  36111  weiunpo  36431  knoppndvlem6  36483  topdifinffinlem  37313  areacirclem4  37671  smprngopr  38012  tsbi1  38093  tsbi2  38094  lkrshpor  39063  2atmat0  39483  dochsnkrlem3  41428  dvrelog2b  42023  aks4d1p1  42033  aks6d1c2p2  42076  hashnexinjle  42086  unitscyglem2  42153  pell1234qrdich  42817  acongid  42932  acongtr  42935  acongrep  42937  acongeq  42940  jm2.23  42953  jm2.25  42956  jm2.27a  42962  kelac2lem  43021  mendvscafval  43147  fzunt1d  43419  rp-fakeimass  43474  frege106d  43717  clsk1indlem3  44005  nanorxor  44274  undif3VD  44853  refsum2cnlem1  44937  reclt0d  45302  limciccioolb  45542  limcicciooub  45558  wallispilem3  45988  fourierdlem35  46063  fourierdlem80  46107  fourierswlem  46151  fouriersw  46152  dfatprc  47045  nltle2tri  47228  icceuelpartlem  47309  requad01  47495  even3prm2  47593  stgoldbwt  47650  clnbgrvtxel  47702  dfclnbgr6  47728  dfnbgr6  47729  dfsclnbgr6  47730  clnbgrgrim  47786  usgrexmpl2trifr  47852  ztprmneprm  48072  altgsumbcALT  48078  zlmodzxznm  48226  zlmodzxzldeplem4  48232  reorelicc  48444  prelrrx2b  48448  rrx2plord1  48455  line2x  48488  itscnhlc0xyqsol  48499  itscnhlinecirc02plem1  48516  fvconst0ci  48572