Theorem orcd 871

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

Syntax hints:   → wi 4   ∨ wo 845

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 846

This theorem is referenced by:  olcd  872  pm2.47  882  orim12i  907  animorl  976  animorrl  979  cases2ALT  1047  sbc2or  3785  rabsnifsb  4725  n0snor2el  4833  disjprgw  5142  disjprg  5143  propeqop  5506  nf1oconst  7299  poxp  8110  xpord2indlem  8129  naddcllem  8671  unxpwdom2  9579  djuunxp  9912  sornom  10268  fin11a  10374  fin56  10384  fin1a2lem11  10401  axdc3lem2  10442  gchdomtri  10620  0tsk  10746  zmulcl  12607  nn0lt2  12621  nn01to3  12921  xrlttri  13114  xmulpnf1  13249  iccsplit  13458  elfznelfzo  13733  hashrabsn01  14329  hashsn01  14372  swrdnnn0nd  14602  zsum  15660  sumsplit  15710  zprod  15877  rpnnen2lem11  16163  lcmfunsnlem2lem1  16571  lcmfunsnlem2  16573  vdwlem6  16915  vdwlem10  16919  cshwshashlem1  17025  basprssdmsets  17153  mreexfidimd  17590  smndex1mgm  18784  sgrp2nmndlem5  18806  symg2bas  19254  psgnunilem1  19355  oppglsm  19504  gsummulgz  19805  prmgrpsimpgd  19978  srgbinomlem4  20045  dvrfval  20208  lringuplu  20306  cnsubrg  20997  marrepfval  22053  marepvfval  22058  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  fctop  22498  cctop  22500  pptbas  22502  metustto  24053  pmltpclem2  24957  dvne0  25519  taylplem2  25867  taylpfval  25868  dvntaylp0  25875  ang180lem3  26305  scvxcvx  26479  lgsdir2lem5  26821  sltres  27154  addsval  27435  mulsval  27554  mulsproplem13  27573  mulsproplem14  27574  tgbtwnconn1  27815  tgbtwnconn2  27816  tgbtwnconn3  27817  legtrid  27831  hltr  27850  hlbtwn  27851  btwnhl1  27852  btwnhl2  27853  tglineneq  27884  ncolncol  27886  colmid  27928  footexALT  27958  footexlem2  27960  colperpexlem3  27972  colperpex  27973  mideulem2  27974  opphllem  27975  hlpasch  27996  hphl  28011  hypcgrlem1  28039  hypcgrlem2  28040  trgcopy  28044  trgcopyeulem  28045  cgracgr  28058  cgraswap  28060  cgrahl  28067  cgracol  28068  inagflat  28080  inaghl  28085  colinearalglem4  28156  axcontlem3  28213  edglnl  28392  clwlkclwwlklem2a  29240  clwwlknonmpo  29331  trlsegvdeg  29469  nfrgr2v  29514  frgrwopreg  29565  frgrreg  29636  ex-natded5.7  29653  ex-natded5.13  29657  ex-natded9.20  29659  ex-natded9.20-2  29660  padct  31931  f1ocnt  32000  linds2eq  32485  submateqlem2  32776  measxun2  33196  measssd  33201  measiun  33204  meascnbl  33205  carsgclctun  33308  satfvsucsuc  34344  fmlasucdisj  34378  satfun  34390  satfv1fvfmla1  34402  2goelgoanfmla1  34403  outsideoftr  35089  lineunray  35107  knoppndvlem6  35381  topdifinffinlem  36216  areacirclem4  36567  smprngopr  36908  tsbi1  36989  tsbi2  36990  lkrshpor  37965  2atmat0  38385  dochsnkrlem3  40330  dvrelog2b  40919  aks4d1p1  40929  aks6d1c2p2  40945  pell1234qrdich  41584  acongid  41699  acongtr  41702  acongrep  41704  acongeq  41707  jm2.23  41720  jm2.25  41723  jm2.27a  41729  kelac2lem  41791  mendvscafval  41917  fzunt1d  42193  rp-fakeimass  42248  frege106d  42491  clsk1indlem3  42779  nanorxor  43049  undif3VD  43628  refsum2cnlem1  43706  reclt0d  44083  limciccioolb  44323  limcicciooub  44339  wallispilem3  44769  fourierdlem35  44844  fourierdlem80  44888  fourierswlem  44932  fouriersw  44933  dfatprc  45824  nltle2tri  46007  icceuelpartlem  46089  requad01  46275  even3prm2  46373  stgoldbwt  46430  isomuspgrlem1  46481  nrhmzr  46633  ztprmneprm  46976  altgsumbcALT  46982  zlmodzxznm  47131  zlmodzxzldeplem4  47137  reorelicc  47349  prelrrx2b  47353  rrx2plord1  47360  line2x  47393  itscnhlc0xyqsol  47404  itscnhlinecirc02plem1  47421  fvconst0ci  47478