Theorem orcd 869

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

Syntax hints:   → wi 4   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  olcd  870  pm2.47  880  orim12i  905  animorl  974  animorrl  977  cases2ALT  1043  sbc2or  3780  rabsnifsb  4657  n0snor2el  4763  disjprgw  5060  disjprg  5061  propeqop  5396  nf1oconst  7059  poxp  7821  unxpwdom2  9051  djuunxp  9349  sornom  9698  fin11a  9804  fin56  9814  fin1a2lem11  9831  axdc3lem2  9872  gchdomtri  10050  0tsk  10176  zmulcl  12030  nn0lt2  12044  nn01to3  12340  xrlttri  12531  xmulpnf1  12666  iccsplit  12870  elfznelfzo  13141  hashrabsn01  13733  hashsn01  13776  swrdnnn0nd  14017  zsum  15074  sumsplit  15122  zprod  15290  rpnnen2lem11  15576  lcmfunsnlem2lem1  15981  lcmfunsnlem2  15983  vdwlem6  16321  vdwlem10  16325  cshwshashlem1  16428  basprssdmsets  16548  mreexfidimd  16920  smndex1mgm  18071  sgrp2nmndlem5  18093  symg2bas  18520  psgnunilem1  18620  oppglsm  18766  gsummulgz  19062  prmgrpsimpgd  19235  srgbinomlem4  19292  dvrfval  19433  cnsubrg  20604  marrepfval  21168  marepvfval  21173  chfacfscmulgsum  21467  chfacfpmmulgsum  21471  fctop  21611  cctop  21613  pptbas  21615  metustto  23162  pmltpclem2  24049  dvne0  24607  taylplem2  24951  taylpfval  24952  dvntaylp0  24959  ang180lem3  25388  scvxcvx  25562  lgsdir2lem5  25904  tgbtwnconn1  26360  tgbtwnconn2  26361  tgbtwnconn3  26362  legtrid  26376  hltr  26395  hlbtwn  26396  btwnhl1  26397  btwnhl2  26398  tglineneq  26429  ncolncol  26431  colmid  26473  footexALT  26503  footexlem2  26505  colperpexlem3  26517  colperpex  26518  mideulem2  26519  opphllem  26520  hlpasch  26541  hphl  26556  hypcgrlem1  26584  hypcgrlem2  26585  trgcopy  26589  trgcopyeulem  26590  cgracgr  26603  cgraswap  26605  cgrahl  26612  cgracol  26613  inagflat  26625  inaghl  26630  colinearalglem4  26694  axcontlem3  26751  edglnl  26927  clwlkclwwlklem2a  27775  clwwlknonmpo  27867  trlsegvdeg  28005  nfrgr2v  28050  frgrwopreg  28101  frgrreg  28172  ex-natded5.7  28189  ex-natded5.13  28193  ex-natded9.20  28195  ex-natded9.20-2  28196  padct  30454  f1ocnt  30524  linds2eq  30941  submateqlem2  31073  measxun2  31469  measssd  31474  measiun  31477  meascnbl  31478  carsgclctun  31579  satfvsucsuc  32612  fmlasucdisj  32646  satfun  32658  satfv1fvfmla1  32670  2goelgoanfmla1  32671  sltres  33169  outsideoftr  33590  lineunray  33608  knoppndvlem6  33856  topdifinffinlem  34627  areacirclem4  34984  smprngopr  35329  tsbi1  35410  tsbi2  35411  lkrshpor  36242  2atmat0  36661  dochsnkrlem3  38606  pell1234qrdich  39456  acongid  39570  acongtr  39573  acongrep  39575  acongeq  39578  jm2.23  39591  jm2.25  39594  jm2.27a  39600  kelac2lem  39662  mendvscafval  39788  rp-fakeimass  39876  frege106d  40098  clsk1indlem3  40391  nanorxor  40635  undif3VD  41214  refsum2cnlem1  41292  reclt0d  41656  limciccioolb  41900  limcicciooub  41916  wallispilem3  42351  fourierdlem35  42426  fourierdlem80  42470  fourierswlem  42514  fouriersw  42515  dfatprc  43328  nltle2tri  43512  icceuelpartlem  43594  requad01  43785  even3prm2  43883  stgoldbwt  43940  isomuspgrlem1  43991  nrhmzr  44143  ztprmneprm  44394  altgsumbcALT  44400  zlmodzxznm  44551  zlmodzxzldeplem4  44557  reorelicc  44696  prelrrx2b  44700  rrx2plord1  44707  line2x  44740  itscnhlc0xyqsol  44751  itscnhlinecirc02plem1  44768