Theorem orcd 887

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  olcd  888  pm2.47  897  orim12i  922  animorl  993  animorrl  996  cases2ALT  1064  sbc2or  3751  rabsnifsb  4686  n0snor2el  4796  disjprg  5103  propeqop  5488  nf1oconst  7310  poxp  8130  xpord2indlem  8149  naddcllem  8668  unxpwdom2  9564  djuunxp  9930  sornom  10283  fin11a  10389  fin56  10399  fin1a2lem11  10416  axdc3lem2  10457  gchdomtri  10642  0tsk  10768  zmulcl  12671  nn0lt2  12688  nn01to3  12994  xrlttri  13194  xmulpnf1  13330  iccsplit  13542  elfznelfzo  13833  fvf1tp  13854  hashrabsn01  14441  hashsn01  14485  swrdnnn0nd  14730  zsum  15808  sumsplit  15858  zprod  16030  rpnnen2lem11  16318  lcmfunsnlem2lem1  16734  lcmfunsnlem2  16736  vdwlem6  17084  vdwlem10  17088  cshwshashlem1  17193  basprssdmsets  17319  mreexfidimd  17744  chnccat  18720  smndex1mgm  19025  sgrp2nmndlem5  19047  symg2bas  19526  psgnunilem1  19626  oppglsm  19775  gsummulgz  20076  prmgrpsimpgd  20249  srgbinomlem4  20374  dvrfval  20549  nrhmzr  20705  lringuplu  20712  isfieldidl  21455  cnsubrg  21646  marrepfval  22788  marepvfval  22793  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  fctop  23235  cctop  23237  pptbas  23239  metustto  24785  pmltpclem2  25683  dvne0  26245  taylplem2  26607  taylpfval  26608  dvntaylp0  26615  ang180lem3  27056  scvxcvx  27230  lgsdir2lem5  27573  ltsres  27906  addsval  28235  mulsval  28382  mulsproplem13  28401  mulsproplem14  28402  oncutlt  28537  n0fincut  28628  zseo  28695  halfcut  28731  z12zsodd  28755  tgbtwnconn1  28925  tgbtwnconn2  28926  tgbtwnconn3  28927  legtrid  28941  hltr  28963  hlbtwn  28964  btwnhl1  28965  btwnhl2  28966  tglineneq  29000  ncolncol  29002  colmid  29047  symquadprlnglem  29052  footexALT  29080  footexlem2  29082  colperpexlem3  29095  colperpex  29096  mideulem2  29097  opphllem  29098  hlpasch  29121  hphl  29136  hlopp  29137  lnincplng  29149  plngrotlem2  29153  symquadmid  29191  hypcgrlem1  29192  hypcgrlem2  29193  trgcopy  29198  trgcopyeulem  29199  cgracgr  29212  cgraswap  29214  cgrahl  29222  cgracol  29223  ragcgra  29230  cgrarag  29231  inagflat  29246  inaghl  29251  angmgmaddeu1  29266  angmgmaddcpbl  29277  prlngref  29305  symquadprlng  29327  colinearalglem4  29374  axcontlem3  29431  edglnl  29608  clwlkclwwlklem2a  30476  clwwlknonmpo  30567  trlsegvdeg  30715  nfrgr2v  30760  frgrwopreg  30811  frgrreg  30882  ex-natded5.7  30899  ex-natded5.13  30903  ex-natded9.20  30905  ex-natded9.20-2  30906  f1ocnt  33279  linds2eq  33822  constrelextdg2  34265  submateqlem2  34326  measxun2  34729  measssd  34734  measiun  34737  meascnbl  34738  carsgclctun  34840  satfvsucsuc  35952  fmlasucdisj  35986  satfun  35998  satfv1fvfmla1  36010  2goelgoanfmla1  36011  outsideoftr  36717  lineunray  36735  weiunpo  37092  knoppndvlem6  37222  topdifinffinlem  38109  areacirclem4  38468  smprngopr  38810  tsbi1  38889  tsbi2  38890  lkrshpor  39988  2atmat0  40407  dochsnkrlem3  42352  dvrelog2b  42940  aks4d1p1  42950  aks6d1c2p2  42993  hashnexinjle  43003  unitscyglem2  43070  pell1234qrdich  43710  acongid  43824  acongtr  43827  acongrep  43829  acongeq  43832  jm2.23  43845  jm2.25  43848  jm2.27a  43854  kelac2lem  43913  mendvscafval  44035  fzunt1d  44305  rp-fakeimass  44360  frege106d  44603  clsk1indlem3  44891  nanorxor  45137  undif3VD  45712  refsum2cnlem1  45879  reclt0d  46224  limciccioolb  46459  limcicciooub  46473  wallispilem3  46903  fourierdlem35  46978  fourierdlem80  47022  fourierswlem  47066  fouriersw  47067  dfatprc  48026  nltle2tri  48209  icceuelpartlem  48343  requad01  48545  even3prm2  48643  stgoldbwt  48700  clnbgrvtxel  48753  dfclnbgr6  48780  dfnbgr6  48781  dfsclnbgr6  48782  clnbgrgrim  48858  usgrexmpl2trifr  48961  gpgusgralem  48980  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpg3nbgrvtx0  49000  gpg3nbgrvtx0ALT  49001  gpg3nbgrvtx1  49002  gpg5edgnedg  49054  smprngprmrng  49262  ztprmneprm  49285  altgsumbcALT  49291  zlmodzxznm  49435  zlmodzxzldeplem4  49441  reorelicc  49648  prelrrx2b  49652  rrx2plord1  49659  line2x  49692  itscnhlc0xyqsol  49703  itscnhlinecirc02plem1  49720  fvconst0ci  49825  upfval  50110