Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30478. (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  3749  rabsnifsb  4679  n0snor2el  4789  disjprg  5094  propeqop  5455  nf1oconst  7251  poxp  8070  xpord2indlem  8089  naddcllem  8604  unxpwdom2  9493  djuunxp  9833  sornom  10187  fin11a  10293  fin56  10303  fin1a2lem11  10320  axdc3lem2  10361  gchdomtri  10540  0tsk  10666  zmulcl  12540  nn0lt2  12555  nn01to3  12854  xrlttri  13053  xmulpnf1  13189  iccsplit  13401  elfznelfzo  13689  fvf1tp  13709  hashrabsn01  14296  hashsn01  14339  swrdnnn0nd  14580  zsum  15641  sumsplit  15691  zprod  15860  rpnnen2lem11  16149  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  vdwlem6  16914  vdwlem10  16918  cshwshashlem1  17023  basprssdmsets  17148  mreexfidimd  17573  chnccat  18549  smndex1mgm  18832  sgrp2nmndlem5  18854  symg2bas  19322  psgnunilem1  19422  oppglsm  19571  gsummulgz  19872  prmgrpsimpgd  20045  srgbinomlem4  20164  dvrfval  20338  nrhmzr  20470  lringuplu  20477  cnsubrg  21382  marrepfval  22504  marepvfval  22509  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  fctop  22948  cctop  22950  pptbas  22952  metustto  24497  pmltpclem2  25406  dvne0  25972  taylplem2  26327  taylpfval  26328  dvntaylp0  26336  ang180lem3  26777  scvxcvx  26952  lgsdir2lem5  27296  ltsres  27630  addsval  27958  mulsval  28105  mulsproplem13  28124  mulsproplem14  28125  oncutlt  28260  n0fincut  28351  zseo  28418  halfcut  28454  z12zsodd  28478  tgbtwnconn1  28647  tgbtwnconn2  28648  tgbtwnconn3  28649  legtrid  28663  hltr  28682  hlbtwn  28683  btwnhl1  28684  btwnhl2  28685  tglineneq  28716  ncolncol  28718  colmid  28760  footexALT  28790  footexlem2  28792  colperpexlem3  28804  colperpex  28805  mideulem2  28806  opphllem  28807  hlpasch  28828  hphl  28843  hypcgrlem1  28871  hypcgrlem2  28872  trgcopy  28876  trgcopyeulem  28877  cgracgr  28890  cgraswap  28892  cgrahl  28899  cgracol  28900  inagflat  28912  inaghl  28917  colinearalglem4  28982  axcontlem3  29039  edglnl  29216  clwlkclwwlklem2a  30073  clwwlknonmpo  30164  trlsegvdeg  30302  nfrgr2v  30347  frgrwopreg  30398  frgrreg  30469  ex-natded5.7  30486  ex-natded5.13  30490  ex-natded9.20  30492  ex-natded9.20-2  30493  padct  32797  f1ocnt  32880  linds2eq  33462  constrelextdg2  33904  submateqlem2  33965  measxun2  34367  measssd  34372  measiun  34375  meascnbl  34376  carsgclctun  34478  satfvsucsuc  35559  fmlasucdisj  35593  satfun  35605  satfv1fvfmla1  35617  2goelgoanfmla1  35618  outsideoftr  36323  lineunray  36341  weiunpo  36659  knoppndvlem6  36717  topdifinffinlem  37548  areacirclem4  37908  smprngopr  38249  tsbi1  38330  tsbi2  38331  lkrshpor  39363  2atmat0  39782  dochsnkrlem3  41727  dvrelog2b  42316  aks4d1p1  42326  aks6d1c2p2  42369  hashnexinjle  42379  unitscyglem2  42446  pell1234qrdich  43099  acongid  43213  acongtr  43216  acongrep  43218  acongeq  43221  jm2.23  43234  jm2.25  43237  jm2.27a  43243  kelac2lem  43302  mendvscafval  43424  fzunt1d  43694  rp-fakeimass  43749  frege106d  43992  clsk1indlem3  44280  nanorxor  44542  undif3VD  45118  refsum2cnlem1  45278  reclt0d  45627  limciccioolb  45863  limcicciooub  45877  wallispilem3  46307  fourierdlem35  46382  fourierdlem80  46426  fourierswlem  46470  fouriersw  46471  squeezedltsq  47128  dfatprc  47372  nltle2tri  47555  icceuelpartlem  47677  requad01  47863  even3prm2  47961  stgoldbwt  48018  clnbgrvtxel  48071  dfclnbgr6  48098  dfnbgr6  48099  dfsclnbgr6  48100  clnbgrgrim  48176  usgrexmpl2trifr  48279  gpgusgralem  48298  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpg3nbgrvtx0  48318  gpg3nbgrvtx0ALT  48319  gpg3nbgrvtx1  48320  gpg5edgnedg  48372  ztprmneprm  48589  altgsumbcALT  48595  zlmodzxznm  48739  zlmodzxzldeplem4  48745  reorelicc  48952  prelrrx2b  48956  rrx2plord1  48963  line2x  48996  itscnhlc0xyqsol  49007  itscnhlinecirc02plem1  49024  fvconst0ci  49132  upfval  49417