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  37596  areacirclem4  37956  smprngopr  38297  tsbi1  38378  tsbi2  38379  lkrshpor  39477  2atmat0  39896  dochsnkrlem3  41841  dvrelog2b  42430  aks4d1p1  42440  aks6d1c2p2  42483  hashnexinjle  42493  unitscyglem2  42560  pell1234qrdich  43212  acongid  43326  acongtr  43329  acongrep  43331  acongeq  43334  jm2.23  43347  jm2.25  43350  jm2.27a  43356  kelac2lem  43415  mendvscafval  43537  fzunt1d  43807  rp-fakeimass  43862  frege106d  44105  clsk1indlem3  44393  nanorxor  44655  undif3VD  45231  refsum2cnlem1  45391  reclt0d  45739  limciccioolb  45975  limcicciooub  45989  wallispilem3  46419  fourierdlem35  46494  fourierdlem80  46538  fourierswlem  46582  fouriersw  46583  squeezedltsq  47240  dfatprc  47484  nltle2tri  47667  icceuelpartlem  47789  requad01  47975  even3prm2  48073  stgoldbwt  48130  clnbgrvtxel  48183  dfclnbgr6  48210  dfnbgr6  48211  dfsclnbgr6  48212  clnbgrgrim  48288  usgrexmpl2trifr  48391  gpgusgralem  48410  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpg3nbgrvtx0  48430  gpg3nbgrvtx0ALT  48431  gpg3nbgrvtx1  48432  gpg5edgnedg  48484  ztprmneprm  48701  altgsumbcALT  48707  zlmodzxznm  48851  zlmodzxzldeplem4  48857  reorelicc  49064  prelrrx2b  49068  rrx2plord1  49075  line2x  49108  itscnhlc0xyqsol  49119  itscnhlinecirc02plem1  49136  fvconst0ci  49244  upfval  49529