Theorem orcd 869

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

This theorem is referenced by:  olcd  870  pm2.47  880  orim12i  905  animorl  974  animorrl  977  cases2ALT  1043  sbc2or  3780  rabsnifsb  4651  n0snor2el  4757  disjprgw  5053  disjprg  5054  propeqop  5389  nf1oconst  7054  poxp  7816  unxpwdom2  9046  djuunxp  9344  sornom  9693  fin11a  9799  fin56  9809  fin1a2lem11  9826  axdc3lem2  9867  gchdomtri  10045  0tsk  10171  zmulcl  12025  nn0lt2  12039  nn01to3  12335  xrlttri  12526  xmulpnf1  12661  iccsplit  12865  elfznelfzo  13136  hashrabsn01  13728  hashsn01  13771  swrdnnn0nd  14012  zsum  15069  sumsplit  15117  zprod  15285  rpnnen2lem11  15571  lcmfunsnlem2lem1  15976  lcmfunsnlem2  15978  vdwlem6  16316  vdwlem10  16320  cshwshashlem1  16423  basprssdmsets  16543  mreexfidimd  16915  smndex1mgm  18066  sgrp2nmndlem5  18088  symg2bas  18515  psgnunilem1  18615  oppglsm  18761  gsummulgz  19057  prmgrpsimpgd  19230  srgbinomlem4  19287  dvrfval  19428  cnsubrg  20599  marrepfval  21163  marepvfval  21168  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  fctop  21606  cctop  21608  pptbas  21610  metustto  23157  pmltpclem2  24044  dvne0  24602  taylplem2  24946  taylpfval  24947  dvntaylp0  24954  ang180lem3  25383  scvxcvx  25557  lgsdir2lem5  25899  tgbtwnconn1  26355  tgbtwnconn2  26356  tgbtwnconn3  26357  legtrid  26371  hltr  26390  hlbtwn  26391  btwnhl1  26392  btwnhl2  26393  tglineneq  26424  ncolncol  26426  colmid  26468  footexALT  26498  footexlem2  26500  colperpexlem3  26512  colperpex  26513  mideulem2  26514  opphllem  26515  hlpasch  26536  hphl  26551  hypcgrlem1  26579  hypcgrlem2  26580  trgcopy  26584  trgcopyeulem  26585  cgracgr  26598  cgraswap  26600  cgrahl  26607  cgracol  26608  inagflat  26620  inaghl  26625  colinearalglem4  26689  axcontlem3  26746  edglnl  26922  clwlkclwwlklem2a  27770  clwwlknonmpo  27862  trlsegvdeg  28000  nfrgr2v  28045  frgrwopreg  28096  frgrreg  28167  ex-natded5.7  28184  ex-natded5.13  28188  ex-natded9.20  28190  ex-natded9.20-2  28191  padct  30449  f1ocnt  30519  linds2eq  30936  submateqlem2  31068  measxun2  31464  measssd  31469  measiun  31472  meascnbl  31473  carsgclctun  31574  satfvsucsuc  32607  fmlasucdisj  32641  satfun  32653  satfv1fvfmla1  32665  2goelgoanfmla1  32666  sltres  33164  outsideoftr  33585  lineunray  33603  knoppndvlem6  33851  topdifinffinlem  34622  areacirclem4  34979  smprngopr  35324  tsbi1  35405  tsbi2  35406  lkrshpor  36237  2atmat0  36656  dochsnkrlem3  38601  pell1234qrdich  39451  acongid  39565  acongtr  39568  acongrep  39570  acongeq  39573  jm2.23  39586  jm2.25  39589  jm2.27a  39595  kelac2lem  39657  mendvscafval  39783  rp-fakeimass  39871  frege106d  40093  clsk1indlem3  40386  nanorxor  40630  undif3VD  41209  refsum2cnlem1  41287  reclt0d  41651  limciccioolb  41895  limcicciooub  41911  wallispilem3  42346  fourierdlem35  42421  fourierdlem80  42465  fourierswlem  42509  fouriersw  42510  dfatprc  43323  nltle2tri  43507  icceuelpartlem  43589  requad01  43780  even3prm2  43878  stgoldbwt  43935  isomuspgrlem1  43986  nrhmzr  44138  ztprmneprm  44389  altgsumbcALT  44395  zlmodzxznm  44546  zlmodzxzldeplem4  44552  reorelicc  44691  prelrrx2b  44695  rrx2plord1  44702  line2x  44735  itscnhlc0xyqsol  44746  itscnhlinecirc02plem1  44763