Theorem orcd 873

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  olcd  874  pm2.47  883  orim12i  908  animorl  979  animorrl  982  cases2ALT  1048  sbc2or  3750  rabsnifsb  4675  n0snor2el  4785  disjprg  5087  propeqop  5447  nf1oconst  7239  poxp  8058  xpord2indlem  8077  naddcllem  8591  unxpwdom2  9474  djuunxp  9814  sornom  10168  fin11a  10274  fin56  10284  fin1a2lem11  10301  axdc3lem2  10342  gchdomtri  10520  0tsk  10646  zmulcl  12521  nn0lt2  12536  nn01to3  12839  xrlttri  13038  xmulpnf1  13173  iccsplit  13385  elfznelfzo  13673  fvf1tp  13693  hashrabsn01  14280  hashsn01  14323  swrdnnn0nd  14564  zsum  15625  sumsplit  15675  zprod  15844  rpnnen2lem11  16133  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  vdwlem6  16898  vdwlem10  16902  cshwshashlem1  17007  basprssdmsets  17132  mreexfidimd  17556  chnccat  18532  smndex1mgm  18815  sgrp2nmndlem5  18837  symg2bas  19306  psgnunilem1  19406  oppglsm  19555  gsummulgz  19856  prmgrpsimpgd  20029  srgbinomlem4  20148  dvrfval  20321  nrhmzr  20453  lringuplu  20460  cnsubrg  21365  marrepfval  22476  marepvfval  22481  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  fctop  22920  cctop  22922  pptbas  22924  metustto  24469  pmltpclem2  25378  dvne0  25944  taylplem2  26299  taylpfval  26300  dvntaylp0  26308  ang180lem3  26749  scvxcvx  26924  lgsdir2lem5  27268  sltres  27602  addsval  27906  mulsval  28049  mulsproplem13  28068  mulsproplem14  28069  onscutlt  28202  n0sfincut  28283  zseo  28346  halfcut  28379  zs12zodd  28393  tgbtwnconn1  28554  tgbtwnconn2  28555  tgbtwnconn3  28556  legtrid  28570  hltr  28589  hlbtwn  28590  btwnhl1  28591  btwnhl2  28592  tglineneq  28623  ncolncol  28625  colmid  28667  footexALT  28697  footexlem2  28699  colperpexlem3  28711  colperpex  28712  mideulem2  28713  opphllem  28714  hlpasch  28735  hphl  28750  hypcgrlem1  28778  hypcgrlem2  28779  trgcopy  28783  trgcopyeulem  28784  cgracgr  28797  cgraswap  28799  cgrahl  28806  cgracol  28807  inagflat  28819  inaghl  28824  colinearalglem4  28888  axcontlem3  28945  edglnl  29122  clwlkclwwlklem2a  29976  clwwlknonmpo  30067  trlsegvdeg  30205  nfrgr2v  30250  frgrwopreg  30301  frgrreg  30372  ex-natded5.7  30389  ex-natded5.13  30393  ex-natded9.20  30395  ex-natded9.20-2  30396  padct  32699  f1ocnt  32780  linds2eq  33344  constrelextdg2  33758  submateqlem2  33819  measxun2  34221  measssd  34226  measiun  34229  meascnbl  34230  carsgclctun  34332  satfvsucsuc  35407  fmlasucdisj  35441  satfun  35453  satfv1fvfmla1  35465  2goelgoanfmla1  35466  outsideoftr  36169  lineunray  36187  weiunpo  36505  knoppndvlem6  36557  topdifinffinlem  37387  areacirclem4  37757  smprngopr  38098  tsbi1  38179  tsbi2  38180  lkrshpor  39152  2atmat0  39571  dochsnkrlem3  41516  dvrelog2b  42105  aks4d1p1  42115  aks6d1c2p2  42158  hashnexinjle  42168  unitscyglem2  42235  pell1234qrdich  42900  acongid  43014  acongtr  43017  acongrep  43019  acongeq  43022  jm2.23  43035  jm2.25  43038  jm2.27a  43044  kelac2lem  43103  mendvscafval  43225  fzunt1d  43496  rp-fakeimass  43551  frege106d  43794  clsk1indlem3  44082  nanorxor  44344  undif3VD  44920  refsum2cnlem1  45080  reclt0d  45431  limciccioolb  45667  limcicciooub  45681  wallispilem3  46111  fourierdlem35  46186  fourierdlem80  46230  fourierswlem  46274  fouriersw  46275  squeezedltsq  46923  dfatprc  47167  nltle2tri  47350  icceuelpartlem  47472  requad01  47658  even3prm2  47756  stgoldbwt  47813  clnbgrvtxel  47866  dfclnbgr6  47893  dfnbgr6  47894  dfsclnbgr6  47895  clnbgrgrim  47971  usgrexmpl2trifr  48074  gpgusgralem  48093  gpg5nbgrvtx03starlem1  48105  gpg5nbgrvtx03starlem2  48106  gpg5nbgrvtx03starlem3  48107  gpg5nbgrvtx13starlem1  48108  gpg5nbgrvtx13starlem2  48109  gpg5nbgrvtx13starlem3  48110  gpg3nbgrvtx0  48113  gpg3nbgrvtx0ALT  48114  gpg3nbgrvtx1  48115  gpg5edgnedg  48167  ztprmneprm  48384  altgsumbcALT  48390  zlmodzxznm  48535  zlmodzxzldeplem4  48541  reorelicc  48748  prelrrx2b  48752  rrx2plord1  48759  line2x  48792  itscnhlc0xyqsol  48803  itscnhlinecirc02plem1  48820  fvconst0ci  48928  upfval  49214