Theorem orcd 869

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 28668. (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 206  df-or 844

This theorem is referenced by:  olcd  870  pm2.47  880  orim12i  905  animorl  974  animorrl  977  cases2ALT  1045  sbc2or  3720  rabsnifsb  4655  n0snor2el  4761  disjprgw  5065  disjprg  5066  propeqop  5415  nf1oconst  7157  poxp  7940  unxpwdom2  9277  djuunxp  9610  sornom  9964  fin11a  10070  fin56  10080  fin1a2lem11  10097  axdc3lem2  10138  gchdomtri  10316  0tsk  10442  zmulcl  12299  nn0lt2  12313  nn01to3  12610  xrlttri  12802  xmulpnf1  12937  iccsplit  13146  elfznelfzo  13420  hashrabsn01  14016  hashsn01  14059  swrdnnn0nd  14297  zsum  15358  sumsplit  15408  zprod  15575  rpnnen2lem11  15861  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  vdwlem6  16615  vdwlem10  16619  cshwshashlem1  16725  basprssdmsets  16853  mreexfidimd  17276  smndex1mgm  18461  sgrp2nmndlem5  18483  symg2bas  18915  psgnunilem1  19016  oppglsm  19162  gsummulgz  19459  prmgrpsimpgd  19632  srgbinomlem4  19694  dvrfval  19841  cnsubrg  20570  marrepfval  21617  marepvfval  21622  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  fctop  22062  cctop  22064  pptbas  22066  metustto  23615  pmltpclem2  24518  dvne0  25080  taylplem2  25428  taylpfval  25429  dvntaylp0  25436  ang180lem3  25866  scvxcvx  26040  lgsdir2lem5  26382  tgbtwnconn1  26840  tgbtwnconn2  26841  tgbtwnconn3  26842  legtrid  26856  hltr  26875  hlbtwn  26876  btwnhl1  26877  btwnhl2  26878  tglineneq  26909  ncolncol  26911  colmid  26953  footexALT  26983  footexlem2  26985  colperpexlem3  26997  colperpex  26998  mideulem2  26999  opphllem  27000  hlpasch  27021  hphl  27036  hypcgrlem1  27064  hypcgrlem2  27065  trgcopy  27069  trgcopyeulem  27070  cgracgr  27083  cgraswap  27085  cgrahl  27092  cgracol  27093  inagflat  27105  inaghl  27110  colinearalglem4  27180  axcontlem3  27237  edglnl  27416  clwlkclwwlklem2a  28263  clwwlknonmpo  28354  trlsegvdeg  28492  nfrgr2v  28537  frgrwopreg  28588  frgrreg  28659  ex-natded5.7  28676  ex-natded5.13  28680  ex-natded9.20  28682  ex-natded9.20-2  28683  padct  30956  f1ocnt  31025  linds2eq  31477  submateqlem2  31660  measxun2  32078  measssd  32083  measiun  32086  meascnbl  32087  carsgclctun  32188  satfvsucsuc  33227  fmlasucdisj  33261  satfun  33273  satfv1fvfmla1  33285  2goelgoanfmla1  33286  xpord2ind  33721  naddcllem  33758  sltres  33792  addsval  34053  outsideoftr  34358  lineunray  34376  knoppndvlem6  34624  topdifinffinlem  35445  areacirclem4  35795  smprngopr  36137  tsbi1  36218  tsbi2  36219  lkrshpor  37048  2atmat0  37467  dochsnkrlem3  39412  dvrelog2b  40002  aks4d1p1  40012  pell1234qrdich  40599  acongid  40713  acongtr  40716  acongrep  40718  acongeq  40721  jm2.23  40734  jm2.25  40737  jm2.27a  40743  kelac2lem  40805  mendvscafval  40931  rp-fakeimass  41017  frege106d  41252  clsk1indlem3  41542  nanorxor  41812  undif3VD  42391  refsum2cnlem1  42469  reclt0d  42816  limciccioolb  43052  limcicciooub  43068  wallispilem3  43498  fourierdlem35  43573  fourierdlem80  43617  fourierswlem  43661  fouriersw  43662  dfatprc  44509  nltle2tri  44693  icceuelpartlem  44775  requad01  44961  even3prm2  45059  stgoldbwt  45116  isomuspgrlem1  45167  nrhmzr  45319  ztprmneprm  45571  altgsumbcALT  45577  zlmodzxznm  45726  zlmodzxzldeplem4  45732  reorelicc  45944  prelrrx2b  45948  rrx2plord1  45955  line2x  45988  itscnhlc0xyqsol  45999  itscnhlinecirc02plem1  46016  fvconst0ci  46074