Theorem orcd 874

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30473. (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  3737  rabsnifsb  4666  n0snor2el  4776  disjprg  5081  propeqop  5461  nf1oconst  7260  poxp  8078  xpord2indlem  8097  naddcllem  8612  unxpwdom2  9503  djuunxp  9845  sornom  10199  fin11a  10305  fin56  10315  fin1a2lem11  10332  axdc3lem2  10373  gchdomtri  10552  0tsk  10678  zmulcl  12576  nn0lt2  12592  nn01to3  12891  xrlttri  13090  xmulpnf1  13226  iccsplit  13438  elfznelfzo  13728  fvf1tp  13748  hashrabsn01  14335  hashsn01  14378  swrdnnn0nd  14619  zsum  15680  sumsplit  15730  zprod  15902  rpnnen2lem11  16191  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  vdwlem6  16957  vdwlem10  16961  cshwshashlem1  17066  basprssdmsets  17191  mreexfidimd  17616  chnccat  18592  smndex1mgm  18878  sgrp2nmndlem5  18900  symg2bas  19368  psgnunilem1  19468  oppglsm  19617  gsummulgz  19918  prmgrpsimpgd  20091  srgbinomlem4  20210  dvrfval  20382  nrhmzr  20514  lringuplu  20521  cnsubrg  21407  marrepfval  22525  marepvfval  22530  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  fctop  22969  cctop  22971  pptbas  22973  metustto  24518  pmltpclem2  25416  dvne0  25978  taylplem2  26329  taylpfval  26330  dvntaylp0  26337  ang180lem3  26775  scvxcvx  26949  lgsdir2lem5  27292  ltsres  27626  addsval  27954  mulsval  28101  mulsproplem13  28120  mulsproplem14  28121  oncutlt  28256  n0fincut  28347  zseo  28414  halfcut  28450  z12zsodd  28474  tgbtwnconn1  28643  tgbtwnconn2  28644  tgbtwnconn3  28645  legtrid  28659  hltr  28678  hlbtwn  28679  btwnhl1  28680  btwnhl2  28681  tglineneq  28712  ncolncol  28714  colmid  28756  footexALT  28786  footexlem2  28788  colperpexlem3  28800  colperpex  28801  mideulem2  28802  opphllem  28803  hlpasch  28824  hphl  28839  hypcgrlem1  28867  hypcgrlem2  28868  trgcopy  28872  trgcopyeulem  28873  cgracgr  28886  cgraswap  28888  cgrahl  28895  cgracol  28896  inagflat  28908  inaghl  28913  colinearalglem4  28978  axcontlem3  29035  edglnl  29212  clwlkclwwlklem2a  30068  clwwlknonmpo  30159  trlsegvdeg  30297  nfrgr2v  30342  frgrwopreg  30393  frgrreg  30464  ex-natded5.7  30481  ex-natded5.13  30485  ex-natded9.20  30487  ex-natded9.20-2  30488  f1ocnt  32873  linds2eq  33441  constrelextdg2  33891  submateqlem2  33952  measxun2  34354  measssd  34359  measiun  34362  meascnbl  34363  carsgclctun  34465  satfvsucsuc  35547  fmlasucdisj  35581  satfun  35593  satfv1fvfmla1  35605  2goelgoanfmla1  35606  outsideoftr  36311  lineunray  36329  weiunpo  36647  knoppndvlem6  36777  topdifinffinlem  37663  areacirclem4  38032  smprngopr  38373  tsbi1  38454  tsbi2  38455  lkrshpor  39553  2atmat0  39972  dochsnkrlem3  41917  dvrelog2b  42505  aks4d1p1  42515  aks6d1c2p2  42558  hashnexinjle  42568  unitscyglem2  42635  pell1234qrdich  43289  acongid  43403  acongtr  43406  acongrep  43408  acongeq  43411  jm2.23  43424  jm2.25  43427  jm2.27a  43433  kelac2lem  43492  mendvscafval  43614  fzunt1d  43884  rp-fakeimass  43939  frege106d  44182  clsk1indlem3  44470  nanorxor  44732  undif3VD  45308  refsum2cnlem1  45468  reclt0d  45816  limciccioolb  46051  limcicciooub  46065  wallispilem3  46495  fourierdlem35  46570  fourierdlem80  46614  fourierswlem  46658  fouriersw  46659  squeezedltsq  47318  dfatprc  47578  nltle2tri  47761  icceuelpartlem  47895  requad01  48097  even3prm2  48195  stgoldbwt  48252  clnbgrvtxel  48305  dfclnbgr6  48332  dfnbgr6  48333  dfsclnbgr6  48334  clnbgrgrim  48410  usgrexmpl2trifr  48513  gpgusgralem  48532  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpg5edgnedg  48606  ztprmneprm  48823  altgsumbcALT  48829  zlmodzxznm  48973  zlmodzxzldeplem4  48979  reorelicc  49186  prelrrx2b  49190  rrx2plord1  49197  line2x  49230  itscnhlc0xyqsol  49241  itscnhlinecirc02plem1  49258  fvconst0ci  49366  upfval  49651