Theorem orcd 873

Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 30383. (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  3745  rabsnifsb  4672  n0snor2el  4782  disjprg  5085  propeqop  5445  nf1oconst  7239  poxp  8058  xpord2indlem  8077  naddcllem  8591  unxpwdom2  9474  djuunxp  9814  sornom  10168  fin11a  10274  fin56  10284  fin1a2lem11  10301  axdc3lem2  10342  gchdomtri  10520  0tsk  10646  zmulcl  12521  nn0lt2  12536  nn01to3  12839  xrlttri  13038  xmulpnf1  13173  iccsplit  13385  elfznelfzo  13673  fvf1tp  13693  hashrabsn01  14280  hashsn01  14323  swrdnnn0nd  14564  zsum  15625  sumsplit  15675  zprod  15844  rpnnen2lem11  16133  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  vdwlem6  16898  vdwlem10  16902  cshwshashlem1  17007  basprssdmsets  17132  mreexfidimd  17556  chnccat  18532  smndex1mgm  18815  sgrp2nmndlem5  18837  symg2bas  19305  psgnunilem1  19405  oppglsm  19554  gsummulgz  19855  prmgrpsimpgd  20028  srgbinomlem4  20147  dvrfval  20320  nrhmzr  20452  lringuplu  20459  cnsubrg  21364  marrepfval  22475  marepvfval  22480  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  fctop  22919  cctop  22921  pptbas  22923  metustto  24468  pmltpclem2  25377  dvne0  25943  taylplem2  26298  taylpfval  26299  dvntaylp0  26307  ang180lem3  26748  scvxcvx  26923  lgsdir2lem5  27267  sltres  27601  addsval  27905  mulsval  28048  mulsproplem13  28067  mulsproplem14  28068  onscutlt  28201  n0sfincut  28282  zseo  28345  halfcut  28378  zs12zodd  28392  tgbtwnconn1  28553  tgbtwnconn2  28554  tgbtwnconn3  28555  legtrid  28569  hltr  28588  hlbtwn  28589  btwnhl1  28590  btwnhl2  28591  tglineneq  28622  ncolncol  28624  colmid  28666  footexALT  28696  footexlem2  28698  colperpexlem3  28710  colperpex  28711  mideulem2  28712  opphllem  28713  hlpasch  28734  hphl  28749  hypcgrlem1  28777  hypcgrlem2  28778  trgcopy  28782  trgcopyeulem  28783  cgracgr  28796  cgraswap  28798  cgrahl  28805  cgracol  28806  inagflat  28818  inaghl  28823  colinearalglem4  28887  axcontlem3  28944  edglnl  29121  clwlkclwwlklem2a  29978  clwwlknonmpo  30069  trlsegvdeg  30207  nfrgr2v  30252  frgrwopreg  30303  frgrreg  30374  ex-natded5.7  30391  ex-natded5.13  30395  ex-natded9.20  30397  ex-natded9.20-2  30398  padct  32701  f1ocnt  32782  linds2eq  33346  constrelextdg2  33760  submateqlem2  33821  measxun2  34223  measssd  34228  measiun  34231  meascnbl  34232  carsgclctun  34334  satfvsucsuc  35409  fmlasucdisj  35443  satfun  35455  satfv1fvfmla1  35467  2goelgoanfmla1  35468  outsideoftr  36173  lineunray  36191  weiunpo  36509  knoppndvlem6  36561  topdifinffinlem  37391  areacirclem4  37761  smprngopr  38102  tsbi1  38183  tsbi2  38184  lkrshpor  39216  2atmat0  39635  dochsnkrlem3  41580  dvrelog2b  42169  aks4d1p1  42179  aks6d1c2p2  42222  hashnexinjle  42232  unitscyglem2  42299  pell1234qrdich  42964  acongid  43078  acongtr  43081  acongrep  43083  acongeq  43086  jm2.23  43099  jm2.25  43102  jm2.27a  43108  kelac2lem  43167  mendvscafval  43289  fzunt1d  43560  rp-fakeimass  43615  frege106d  43858  clsk1indlem3  44146  nanorxor  44408  undif3VD  44984  refsum2cnlem1  45144  reclt0d  45495  limciccioolb  45731  limcicciooub  45745  wallispilem3  46175  fourierdlem35  46250  fourierdlem80  46294  fourierswlem  46338  fouriersw  46339  squeezedltsq  46996  dfatprc  47240  nltle2tri  47423  icceuelpartlem  47545  requad01  47731  even3prm2  47829  stgoldbwt  47886  clnbgrvtxel  47939  dfclnbgr6  47966  dfnbgr6  47967  dfsclnbgr6  47968  clnbgrgrim  48044  usgrexmpl2trifr  48147  gpgusgralem  48166  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  gpg3nbgrvtx0  48186  gpg3nbgrvtx0ALT  48187  gpg3nbgrvtx1  48188  gpg5edgnedg  48240  ztprmneprm  48457  altgsumbcALT  48463  zlmodzxznm  48608  zlmodzxzldeplem4  48614  reorelicc  48821  prelrrx2b  48825  rrx2plord1  48832  line2x  48865  itscnhlc0xyqsol  48876  itscnhlinecirc02plem1  48893  fvconst0ci  49001  upfval  49287