Theorem orcd 887

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30791. (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  3756  rabsnifsb  4693  n0snor2el  4803  disjprg  5110  propeqop  5495  nf1oconst  7314  poxp  8133  xpord2indlem  8152  naddcllem  8671  unxpwdom2  9560  djuunxp  9926  sornom  10279  fin11a  10385  fin56  10395  fin1a2lem11  10412  axdc3lem2  10453  gchdomtri  10632  0tsk  10758  zmulcl  12661  nn0lt2  12677  nn01to3  12983  xrlttri  13182  xmulpnf1  13318  iccsplit  13530  elfznelfzo  13821  fvf1tp  13842  hashrabsn01  14429  hashsn01  14473  swrdnnn0nd  14718  zsum  15795  sumsplit  15845  zprod  16017  rpnnen2lem11  16305  lcmfunsnlem2lem1  16721  lcmfunsnlem2  16723  vdwlem6  17071  vdwlem10  17075  cshwshashlem1  17180  basprssdmsets  17306  mreexfidimd  17731  chnccat  18707  smndex1mgm  19000  sgrp2nmndlem5  19022  symg2bas  19494  psgnunilem1  19594  oppglsm  19743  gsummulgz  20044  prmgrpsimpgd  20217  srgbinomlem4  20342  dvrfval  20517  nrhmzr  20673  lringuplu  20680  isfieldidl  21423  cnsubrg  21614  marrepfval  22754  marepvfval  22759  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  fctop  23198  cctop  23200  pptbas  23202  metustto  24747  pmltpclem2  25645  dvne0  26207  taylplem2  26564  taylpfval  26565  dvntaylp0  26572  ang180lem3  27013  scvxcvx  27187  lgsdir2lem5  27530  ltsres  27863  addsval  28192  mulsval  28339  mulsproplem13  28358  mulsproplem14  28359  oncutlt  28494  n0fincut  28585  zseo  28652  halfcut  28688  z12zsodd  28712  tgbtwnconn1  28881  tgbtwnconn2  28882  tgbtwnconn3  28883  legtrid  28897  hltr  28919  hlbtwn  28920  btwnhl1  28921  btwnhl2  28922  tglineneq  28955  ncolncol  28957  colmid  29002  symquadprlnglem  29007  footexALT  29035  footexlem2  29037  colperpexlem3  29050  colperpex  29051  mideulem2  29052  opphllem  29053  hlpasch  29075  hphl  29090  hlopp  29091  lnincplng  29103  plngrotlem2  29107  symquadmid  29145  hypcgrlem1  29146  hypcgrlem2  29147  trgcopy  29152  trgcopyeulem  29153  cgracgr  29166  cgraswap  29168  cgrahl  29175  cgracol  29176  ragcgra  29183  cgrarag  29184  inagflat  29194  inaghl  29199  prlngref  29227  symquadprlng  29249  colinearalglem4  29296  axcontlem3  29353  edglnl  29530  clwlkclwwlklem2a  30386  clwwlknonmpo  30477  trlsegvdeg  30615  nfrgr2v  30660  frgrwopreg  30711  frgrreg  30782  ex-natded5.7  30799  ex-natded5.13  30803  ex-natded9.20  30805  ex-natded9.20-2  30806  f1ocnt  33182  linds2eq  33725  constrelextdg2  34168  submateqlem2  34229  measxun2  34632  measssd  34637  measiun  34640  meascnbl  34641  carsgclctun  34743  satfvsucsuc  35878  fmlasucdisj  35912  satfun  35924  satfv1fvfmla1  35936  2goelgoanfmla1  35937  outsideoftr  36642  lineunray  36660  weiunpo  37017  knoppndvlem6  37147  topdifinffinlem  38034  areacirclem4  38403  smprngopr  38744  tsbi1  38823  tsbi2  38824  lkrshpor  39922  2atmat0  40341  dochsnkrlem3  42286  dvrelog2b  42874  aks4d1p1  42884  aks6d1c2p2  42927  hashnexinjle  42937  unitscyglem2  43004  pell1234qrdich  43629  acongid  43743  acongtr  43746  acongrep  43748  acongeq  43751  jm2.23  43764  jm2.25  43767  jm2.27a  43773  kelac2lem  43832  mendvscafval  43954  fzunt1d  44224  rp-fakeimass  44279  frege106d  44522  clsk1indlem3  44810  nanorxor  45056  undif3VD  45631  refsum2cnlem1  45798  reclt0d  46143  limciccioolb  46378  limcicciooub  46392  wallispilem3  46822  fourierdlem35  46897  fourierdlem80  46941  fourierswlem  46985  fouriersw  46986  squeezedltsq  47644  dfatprc  47908  nltle2tri  48091  icceuelpartlem  48225  requad01  48427  even3prm2  48525  stgoldbwt  48582  clnbgrvtxel  48635  dfclnbgr6  48662  dfnbgr6  48663  dfsclnbgr6  48664  clnbgrgrim  48740  usgrexmpl2trifr  48843  gpgusgralem  48862  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpg3nbgrvtx0  48882  gpg3nbgrvtx0ALT  48883  gpg3nbgrvtx1  48884  gpg5edgnedg  48936  smprngprmrng  49145  ztprmneprm  49168  altgsumbcALT  49174  zlmodzxznm  49318  zlmodzxzldeplem4  49324  reorelicc  49531  prelrrx2b  49535  rrx2plord1  49542  line2x  49575  itscnhlc0xyqsol  49586  itscnhlinecirc02plem1  49603  fvconst0ci  49710  upfval  49995