Theorem orcd 886

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

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

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 861

This theorem is used by:  olcd  887  pm2.47  896  orim12i  921  animorl  993  animorrl  996  cases2ALT  1064  sbc2or  3753  rabsnifsb  4688  n0snor2el  4798  disjprg  5105  propeqop  5490  nf1oconst  7303  poxp  8120  xpord2indlem  8139  naddcllem  8658  unxpwdom2  9546  djuunxp  9912  sornom  10265  fin11a  10371  fin56  10381  fin1a2lem11  10398  axdc3lem2  10439  gchdomtri  10618  0tsk  10744  zmulcl  12647  nn0lt2  12663  nn01to3  12969  xrlttri  13168  xmulpnf1  13304  iccsplit  13516  elfznelfzo  13807  fvf1tp  13827  hashrabsn01  14414  hashsn01  14458  swrdnnn0nd  14699  zsum  15774  sumsplit  15824  zprod  15996  rpnnen2lem11  16284  lcmfunsnlem2lem1  16700  lcmfunsnlem2  16702  vdwlem6  17050  vdwlem10  17054  cshwshashlem1  17159  basprssdmsets  17285  mreexfidimd  17710  chnccat  18686  smndex1mgm  18973  sgrp2nmndlem5  18995  symg2bas  19467  psgnunilem1  19567  oppglsm  19716  gsummulgz  20017  prmgrpsimpgd  20190  srgbinomlem4  20315  dvrfval  20489  nrhmzr  20645  lringuplu  20652  isfieldidl  21395  cnsubrg  21586  marrepfval  22726  marepvfval  22731  chfacfscmulgsum  23026  chfacfpmmulgsum  23030  fctop  23170  cctop  23172  pptbas  23174  metustto  24719  pmltpclem2  25617  dvne0  26179  taylplem2  26536  taylpfval  26537  dvntaylp0  26544  ang180lem3  26985  scvxcvx  27159  lgsdir2lem5  27502  ltsres  27835  addsval  28164  mulsval  28311  mulsproplem13  28330  mulsproplem14  28331  oncutlt  28466  n0fincut  28557  zseo  28624  halfcut  28660  z12zsodd  28684  tgbtwnconn1  28853  tgbtwnconn2  28854  tgbtwnconn3  28855  legtrid  28869  hltr  28891  hlbtwn  28892  btwnhl1  28893  btwnhl2  28894  tglineneq  28927  ncolncol  28929  colmid  28974  symquadprlnglem  28979  footexALT  29007  footexlem2  29009  colperpexlem3  29022  colperpex  29023  mideulem2  29024  opphllem  29025  hlpasch  29047  hphl  29062  hlopp  29063  lnincplng  29075  plngrotlem2  29079  symquadmid  29117  hypcgrlem1  29118  hypcgrlem2  29119  trgcopy  29124  trgcopyeulem  29125  cgracgr  29138  cgraswap  29140  cgrahl  29147  cgracol  29148  ragcgra  29155  cgrarag  29156  inagflat  29166  inaghl  29171  prlngref  29199  symquadprlng  29221  colinearalglem4  29268  axcontlem3  29325  edglnl  29502  clwlkclwwlklem2a  30358  clwwlknonmpo  30449  trlsegvdeg  30587  nfrgr2v  30632  frgrwopreg  30683  frgrreg  30754  ex-natded5.7  30771  ex-natded5.13  30775  ex-natded9.20  30777  ex-natded9.20-2  30778  f1ocnt  33154  linds2eq  33703  constrelextdg2  34146  submateqlem2  34207  measxun2  34609  measssd  34614  measiun  34617  meascnbl  34618  carsgclctun  34720  satfvsucsuc  35865  fmlasucdisj  35899  satfun  35911  satfv1fvfmla1  35923  2goelgoanfmla1  35924  outsideoftr  36629  lineunray  36647  weiunpo  37004  knoppndvlem6  37134  topdifinffinlem  38021  areacirclem4  38390  smprngopr  38731  tsbi1  38810  tsbi2  38811  lkrshpor  39909  2atmat0  40328  dochsnkrlem3  42273  dvrelog2b  42861  aks4d1p1  42871  aks6d1c2p2  42914  hashnexinjle  42924  unitscyglem2  42991  pell1234qrdich  43616  acongid  43730  acongtr  43733  acongrep  43735  acongeq  43738  jm2.23  43751  jm2.25  43754  jm2.27a  43760  kelac2lem  43819  mendvscafval  43941  fzunt1d  44211  rp-fakeimass  44266  frege106d  44509  clsk1indlem3  44797  nanorxor  45043  undif3VD  45618  refsum2cnlem1  45785  reclt0d  46130  limciccioolb  46365  limcicciooub  46379  wallispilem3  46809  fourierdlem35  46884  fourierdlem80  46928  fourierswlem  46972  fouriersw  46973  squeezedltsq  47631  dfatprc  47895  nltle2tri  48078  icceuelpartlem  48212  requad01  48414  even3prm2  48512  stgoldbwt  48569  clnbgrvtxel  48622  dfclnbgr6  48649  dfnbgr6  48650  dfsclnbgr6  48651  clnbgrgrim  48727  usgrexmpl2trifr  48830  gpgusgralem  48849  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  gpg3nbgrvtx0  48869  gpg3nbgrvtx0ALT  48870  gpg3nbgrvtx1  48871  gpg5edgnedg  48923  smprngprmrng  49132  ztprmneprm  49155  altgsumbcALT  49161  zlmodzxznm  49305  zlmodzxzldeplem4  49311  reorelicc  49518  prelrrx2b  49522  rrx2plord1  49529  line2x  49562  itscnhlc0xyqsol  49573  itscnhlinecirc02plem1  49590  fvconst0ci  49697  upfval  49982