Theorem orcd 872

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 29656. (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 206  df-or 847

This theorem is referenced by:  olcd  873  pm2.47  883  orim12i  908  animorl  977  animorrl  980  cases2ALT  1048  sbc2or  3787  rabsnifsb  4727  n0snor2el  4835  disjprgw  5144  disjprg  5145  propeqop  5508  nf1oconst  7303  poxp  8114  xpord2indlem  8133  naddcllem  8675  unxpwdom2  9583  djuunxp  9916  sornom  10272  fin11a  10378  fin56  10388  fin1a2lem11  10405  axdc3lem2  10446  gchdomtri  10624  0tsk  10750  zmulcl  12611  nn0lt2  12625  nn01to3  12925  xrlttri  13118  xmulpnf1  13253  iccsplit  13462  elfznelfzo  13737  hashrabsn01  14333  hashsn01  14376  swrdnnn0nd  14606  zsum  15664  sumsplit  15714  zprod  15881  rpnnen2lem11  16167  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  vdwlem6  16919  vdwlem10  16923  cshwshashlem1  17029  basprssdmsets  17157  mreexfidimd  17594  smndex1mgm  18788  sgrp2nmndlem5  18810  symg2bas  19260  psgnunilem1  19361  oppglsm  19510  gsummulgz  19811  prmgrpsimpgd  19984  srgbinomlem4  20052  dvrfval  20216  lringuplu  20314  cnsubrg  21005  marrepfval  22062  marepvfval  22067  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  fctop  22507  cctop  22509  pptbas  22511  metustto  24062  pmltpclem2  24966  dvne0  25528  taylplem2  25876  taylpfval  25877  dvntaylp0  25884  ang180lem3  26316  scvxcvx  26490  lgsdir2lem5  26832  sltres  27165  addsval  27446  mulsval  27565  mulsproplem13  27584  mulsproplem14  27585  tgbtwnconn1  27826  tgbtwnconn2  27827  tgbtwnconn3  27828  legtrid  27842  hltr  27861  hlbtwn  27862  btwnhl1  27863  btwnhl2  27864  tglineneq  27895  ncolncol  27897  colmid  27939  footexALT  27969  footexlem2  27971  colperpexlem3  27983  colperpex  27984  mideulem2  27985  opphllem  27986  hlpasch  28007  hphl  28022  hypcgrlem1  28050  hypcgrlem2  28051  trgcopy  28055  trgcopyeulem  28056  cgracgr  28069  cgraswap  28071  cgrahl  28078  cgracol  28079  inagflat  28091  inaghl  28096  colinearalglem4  28167  axcontlem3  28224  edglnl  28403  clwlkclwwlklem2a  29251  clwwlknonmpo  29342  trlsegvdeg  29480  nfrgr2v  29525  frgrwopreg  29576  frgrreg  29647  ex-natded5.7  29664  ex-natded5.13  29668  ex-natded9.20  29670  ex-natded9.20-2  29671  padct  31944  f1ocnt  32013  linds2eq  32497  submateqlem2  32788  measxun2  33208  measssd  33213  measiun  33216  meascnbl  33217  carsgclctun  33320  satfvsucsuc  34356  fmlasucdisj  34390  satfun  34402  satfv1fvfmla1  34414  2goelgoanfmla1  34415  outsideoftr  35101  lineunray  35119  knoppndvlem6  35393  topdifinffinlem  36228  areacirclem4  36579  smprngopr  36920  tsbi1  37001  tsbi2  37002  lkrshpor  37977  2atmat0  38397  dochsnkrlem3  40342  dvrelog2b  40931  aks4d1p1  40941  aks6d1c2p2  40957  pell1234qrdich  41599  acongid  41714  acongtr  41717  acongrep  41719  acongeq  41722  jm2.23  41735  jm2.25  41738  jm2.27a  41744  kelac2lem  41806  mendvscafval  41932  fzunt1d  42208  rp-fakeimass  42263  frege106d  42506  clsk1indlem3  42794  nanorxor  43064  undif3VD  43643  refsum2cnlem1  43721  reclt0d  44097  limciccioolb  44337  limcicciooub  44353  wallispilem3  44783  fourierdlem35  44858  fourierdlem80  44902  fourierswlem  44946  fouriersw  44947  dfatprc  45838  nltle2tri  46021  icceuelpartlem  46103  requad01  46289  even3prm2  46387  stgoldbwt  46444  isomuspgrlem1  46495  nrhmzr  46647  ztprmneprm  47023  altgsumbcALT  47029  zlmodzxznm  47178  zlmodzxzldeplem4  47184  reorelicc  47396  prelrrx2b  47400  rrx2plord1  47407  line2x  47440  itscnhlc0xyqsol  47451  itscnhlinecirc02plem1  47468  fvconst0ci  47525