Theorem orcd 874

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  olcd  875  pm2.47  884  orim12i  909  animorl  980  animorrl  983  cases2ALT  1049  sbc2or  3751  rabsnifsb  4681  n0snor2el  4791  disjprg  5096  propeqop  5463  nf1oconst  7261  poxp  8080  xpord2indlem  8099  naddcllem  8614  unxpwdom2  9505  djuunxp  9845  sornom  10199  fin11a  10305  fin56  10315  fin1a2lem11  10332  axdc3lem2  10373  gchdomtri  10552  0tsk  10678  zmulcl  12552  nn0lt2  12567  nn01to3  12866  xrlttri  13065  xmulpnf1  13201  iccsplit  13413  elfznelfzo  13701  fvf1tp  13721  hashrabsn01  14308  hashsn01  14351  swrdnnn0nd  14592  zsum  15653  sumsplit  15703  zprod  15872  rpnnen2lem11  16161  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  vdwlem6  16926  vdwlem10  16930  cshwshashlem1  17035  basprssdmsets  17160  mreexfidimd  17585  chnccat  18561  smndex1mgm  18844  sgrp2nmndlem5  18866  symg2bas  19334  psgnunilem1  19434  oppglsm  19583  gsummulgz  19884  prmgrpsimpgd  20057  srgbinomlem4  20176  dvrfval  20350  nrhmzr  20482  lringuplu  20489  cnsubrg  21394  marrepfval  22516  marepvfval  22521  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  fctop  22960  cctop  22962  pptbas  22964  metustto  24509  pmltpclem2  25418  dvne0  25984  taylplem2  26339  taylpfval  26340  dvntaylp0  26348  ang180lem3  26789  scvxcvx  26964  lgsdir2lem5  27308  ltsres  27642  addsval  27970  mulsval  28117  mulsproplem13  28136  mulsproplem14  28137  oncutlt  28272  n0fincut  28363  zseo  28430  halfcut  28466  z12zsodd  28490  tgbtwnconn1  28659  tgbtwnconn2  28660  tgbtwnconn3  28661  legtrid  28675  hltr  28694  hlbtwn  28695  btwnhl1  28696  btwnhl2  28697  tglineneq  28728  ncolncol  28730  colmid  28772  footexALT  28802  footexlem2  28804  colperpexlem3  28816  colperpex  28817  mideulem2  28818  opphllem  28819  hlpasch  28840  hphl  28855  hypcgrlem1  28883  hypcgrlem2  28884  trgcopy  28888  trgcopyeulem  28889  cgracgr  28902  cgraswap  28904  cgrahl  28911  cgracol  28912  inagflat  28924  inaghl  28929  colinearalglem4  28994  axcontlem3  29051  edglnl  29228  clwlkclwwlklem2a  30085  clwwlknonmpo  30176  trlsegvdeg  30314  nfrgr2v  30359  frgrwopreg  30410  frgrreg  30481  ex-natded5.7  30498  ex-natded5.13  30502  ex-natded9.20  30504  ex-natded9.20-2  30505  padct  32807  f1ocnt  32890  linds2eq  33473  constrelextdg2  33924  submateqlem2  33985  measxun2  34387  measssd  34392  measiun  34395  meascnbl  34396  carsgclctun  34498  satfvsucsuc  35578  fmlasucdisj  35612  satfun  35624  satfv1fvfmla1  35636  2goelgoanfmla1  35637  outsideoftr  36342  lineunray  36360  weiunpo  36678  knoppndvlem6  36736  topdifinffinlem  37599  areacirclem4  37959  smprngopr  38300  tsbi1  38381  tsbi2  38382  lkrshpor  39480  2atmat0  39899  dochsnkrlem3  41844  dvrelog2b  42433  aks4d1p1  42443  aks6d1c2p2  42486  hashnexinjle  42496  unitscyglem2  42563  pell1234qrdich  43215  acongid  43329  acongtr  43332  acongrep  43334  acongeq  43337  jm2.23  43350  jm2.25  43353  jm2.27a  43359  kelac2lem  43418  mendvscafval  43540  fzunt1d  43810  rp-fakeimass  43865  frege106d  44108  clsk1indlem3  44396  nanorxor  44658  undif3VD  45234  refsum2cnlem1  45394  reclt0d  45742  limciccioolb  45978  limcicciooub  45992  wallispilem3  46422  fourierdlem35  46497  fourierdlem80  46541  fourierswlem  46585  fouriersw  46586  squeezedltsq  47243  dfatprc  47487  nltle2tri  47670  icceuelpartlem  47792  requad01  47978  even3prm2  48076  stgoldbwt  48133  clnbgrvtxel  48186  dfclnbgr6  48213  dfnbgr6  48214  dfsclnbgr6  48215  clnbgrgrim  48291  usgrexmpl2trifr  48394  gpgusgralem  48413  gpg5nbgrvtx03starlem1  48425  gpg5nbgrvtx03starlem2  48426  gpg5nbgrvtx03starlem3  48427  gpg5nbgrvtx13starlem1  48428  gpg5nbgrvtx13starlem2  48429  gpg5nbgrvtx13starlem3  48430  gpg3nbgrvtx0  48433  gpg3nbgrvtx0ALT  48434  gpg3nbgrvtx1  48435  gpg5edgnedg  48487  ztprmneprm  48704  altgsumbcALT  48710  zlmodzxznm  48854  zlmodzxzldeplem4  48860  reorelicc  49067  prelrrx2b  49071  rrx2plord1  49078  line2x  49111  itscnhlc0xyqsol  49122  itscnhlinecirc02plem1  49139  fvconst0ci  49247  upfval  49532