Theorem orcd 870

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

Syntax hints:   → wi 4   ∨ wo 842

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 208  df-or 843

This theorem is referenced by:  olcd  871  pm2.47  878  orim12i  903  animorl  972  animorrl  975  cases2ALT  1041  sbc2or  3715  rabsnifsb  4565  n0snor2el  4671  disjprg  4958  propeqop  5288  poxp  7675  unxpwdom2  8898  djuunxp  9196  sornom  9545  fin11a  9651  fin56  9661  fin1a2lem11  9678  axdc3lem2  9719  gchdomtri  9897  0tsk  10023  zmulcl  11880  nn0lt2  11894  nn01to3  12190  xrlttri  12382  xmulpnf1  12517  iccsplit  12721  elfznelfzo  12992  hashrabsn01  13582  hashsn01  13625  swrdnnn0nd  13854  zsum  14908  sumsplit  14956  zprod  15124  rpnnen2lem11  15410  lcmfunsnlem2lem1  15811  lcmfunsnlem2  15813  vdwlem6  16151  vdwlem10  16155  cshwshashlem1  16258  basprssdmsets  16378  mreexfidimd  16750  sgrp2nmndlem5  17855  symg2bas  18257  psgnunilem1  18352  gsummulgz  18783  srgbinomlem4  18983  cnsubrg  20287  chfacfscmulgsum  21152  chfacfpmmulgsum  21156  fctop  21296  cctop  21298  pptbas  21300  metustto  22846  pmltpclem2  23733  dvne0  24291  taylplem2  24635  taylpfval  24636  dvntaylp0  24643  ang180lem3  25070  scvxcvx  25245  lgsdir2lem5  25587  tgbtwnconn1  26043  tgbtwnconn2  26044  tgbtwnconn3  26045  legtrid  26059  hltr  26078  hlbtwn  26079  btwnhl1  26080  btwnhl2  26081  tglineneq  26112  ncolncol  26114  colmid  26156  footexALT  26186  footexlem2  26188  colperpexlem3  26200  colperpex  26201  mideulem2  26202  opphllem  26203  hlpasch  26224  hphl  26239  hypcgrlem1  26267  hypcgrlem2  26268  trgcopy  26272  trgcopyeulem  26273  cgracgr  26286  cgraswap  26288  cgrahl  26295  cgracol  26296  inagflat  26309  inaghl  26314  colinearalglem4  26378  axcontlem3  26435  edglnl  26611  clwlkclwwlklem2a  27463  trlsegvdeg  27694  nfrgr2v  27743  frgrwopreg  27794  frgrreg  27865  ex-natded5.7  27882  ex-natded5.13  27886  ex-natded9.20  27888  ex-natded9.20-2  27889  padct  30143  f1ocnt  30209  linds2eq  30587  submateqlem2  30688  measxun2  31086  measssd  31091  measiun  31094  meascnbl  31095  carsgclctun  31196  satfvsucsuc  32220  fmlasucdisj  32254  satfun  32266  satfv1fvfmla1  32278  2goelgoanfmla1  32279  sltres  32778  outsideoftr  33199  lineunray  33217  knoppndvlem6  33465  topdifinffinlem  34159  areacirclem4  34516  smprngopr  34862  tsbi1  34943  tsbi2  34944  lkrshpor  35774  2atmat0  36193  dochsnkrlem3  38138  pell1234qrdich  38943  acongid  39057  acongtr  39060  acongrep  39062  acongeq  39065  jm2.23  39078  jm2.25  39081  jm2.27a  39087  kelac2lem  39149  rp-fakeimass  39363  frege106d  39585  clsk1indlem3  39878  prmgrpsimpgd  40171  nanorxor  40175  undif3VD  40755  refsum2cnlem1  40833  reclt0d  41199  limciccioolb  41444  limcicciooub  41460  wallispilem3  41894  fourierdlem35  41969  fourierdlem80  42013  fourierswlem  42057  fouriersw  42058  dfatprc  42845  nltle2tri  43029  icceuelpartlem  43077  requad01  43268  even3prm2  43366  stgoldbwt  43423  isomuspgrlem1  43474  nrhmzr  43622  ztprmneprm  43873  altgsumbcALT  43879  zlmodzxznm  44032  zlmodzxzldeplem4  44038  reorelicc  44178  prelrrx2b  44182  rrx2plord1  44189  line2x  44222  itscnhlc0xyqsol  44233  itscnhlinecirc02plem1  44250