Theorem orcd 406

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

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  olcd  407  pm2.47  413  animorl  504  animorrl  507  orim12i  537  cases2  1005  sbc2or  3411  undif3OLD  3848  rabsnifsb  4201  n0snor2el  4304  disjprg  4578  propeqop  4895  poxp  7176  unxpwdom2  8376  sornom  8982  fin11a  9088  fin56  9098  fin1a2lem11  9115  axdc3lem2  9156  gchdomtri  9330  0tsk  9456  zmulcl  11303  nn0lt2  11317  nn01to3  11657  xrlttri  11848  xmulpnf1  11976  iccsplit  12176  elfznelfzo  12439  hashrabsn01  13023  hashsn01  13065  ccatsymb  13219  zsum  14296  sumsplit  14341  zprod  14506  rpnnen2lem11  14792  sadadd2lem2  15010  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  vdwlem6  15528  vdwlem10  15532  cshwshashlem1  15640  mreexexlem4d  16130  mreexfidimd  16134  sgrp2nmndlem5  17239  symg2bas  17641  psgnunilem1  17736  gsummulgz  18166  srgbinomlem4  18366  drngnidl  19050  cnsubrg  19625  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  fctop  20618  cctop  20620  ppttop  20621  pptbas  20622  metustto  22168  pmltpclem2  23025  dvne0  23578  taylplem2  23922  taylpfval  23923  dvntaylp0  23930  ang180lem3  24341  scvxcvx  24512  wilthlem2  24595  lgsdir2lem5  24854  tgbtwnconn1  25270  tgbtwnconn2  25271  tgbtwnconn3  25272  legtrid  25286  hltr  25305  hlbtwn  25306  btwnhl1  25307  btwnhl2  25308  tglineneq  25339  ncolncol  25341  colmid  25383  footex  25413  colperpexlem3  25424  colperpex  25425  mideulem2  25426  opphllem  25427  hlpasch  25448  colhp  25462  hphl  25463  hypcgrlem1  25491  hypcgrlem2  25492  trgcopy  25496  trgcopyeulem  25497  cgracgr  25510  cgraswap  25512  cgrahl  25518  cgracol  25519  inaghl  25531  colinearalglem4  25589  axcontlem3  25646  uhgrstrrepelem  25744  clwlkisclwwlklem2a  26313  frgra2v  26526  frgrawopreg  26576  2spotiundisj  26589  frgrareg  26644  ex-natded5.7  26660  ex-natded5.13  26664  ex-natded9.20  26666  ex-natded9.20-2  26667  padct  28885  f1ocnt  28946  submateqlem2  29202  measxun2  29600  measssd  29605  measiun  29608  meascnbl  29609  carsgclctun  29710  sltres  31061  nobnddown  31100  outsideoftr  31406  lineunray  31424  knoppndvlem6  31678  topdifinffinlem  32371  areacirclem4  32673  smprngopr  33021  tsbi1  33110  tsbi2  33111  lkrshpor  33412  2atmat0  33830  dochsnkrlem3  35778  pell1234qrdich  36443  acongid  36560  acongtr  36563  acongrep  36565  acongeq  36568  jm2.23  36581  jm2.25  36584  jm2.27a  36590  kelac2lem  36652  rp-fakeimass  36876  frege106d  37066  clsk1indlem3  37361  nanorxor  37526  undif3VD  38140  refsum2cnlem1  38219  reclt0d  38548  limciccioolb  38688  limcicciooub  38704  wallispilem3  38960  fourierdlem35  39035  fourierdlem80  39079  fourierswlem  39123  fouriersw  39124  nltle2tri  39942  icceuelpartlem  39973  stgoldbwt  40198  clwlkclwwlklem2a  41207  trlsegvdeg  41395  nfrgr2v  41442  frgrwopreg  41486  av-frgrareg  41548  nrhmzr  41663  ztprmneprm  41918  altgsumbcALT  41924  lindslinindsimp1  42040  zlmodzxznm  42080  zlmodzxzldeplem4  42086