Theorem orcd 886

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  olcd  887  pm2.47  896  orim12i  921  animorl  993  animorrl  996  cases2ALT  1064  sbc2or  3754  rabsnifsb  4689  n0snor2el  4799  disjprg  5106  propeqop  5492  nf1oconst  7305  poxp  8125  xpord2indlem  8144  naddcllem  8663  unxpwdom2  9551  djuunxp  9908  sornom  10262  fin11a  10368  fin56  10378  fin1a2lem11  10395  axdc3lem2  10436  gchdomtri  10615  0tsk  10741  zmulcl  12644  nn0lt2  12660  nn01to3  12966  xrlttri  13165  xmulpnf1  13301  iccsplit  13513  elfznelfzo  13804  fvf1tp  13824  hashrabsn01  14411  hashsn01  14455  swrdnnn0nd  14696  zsum  15771  sumsplit  15821  zprod  15993  rpnnen2lem11  16281  lcmfunsnlem2lem1  16697  lcmfunsnlem2  16699  vdwlem6  17047  vdwlem10  17051  cshwshashlem1  17156  basprssdmsets  17282  mreexfidimd  17707  chnccat  18683  smndex1mgm  18970  sgrp2nmndlem5  18992  symg2bas  19464  psgnunilem1  19564  oppglsm  19713  gsummulgz  20014  prmgrpsimpgd  20187  srgbinomlem4  20312  dvrfval  20485  nrhmzr  20623  lringuplu  20630  isfieldidl  21367  cnsubrg  21558  marrepfval  22698  marepvfval  22703  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  fctop  23142  cctop  23144  pptbas  23146  metustto  24691  pmltpclem2  25589  dvne0  26151  taylplem2  26508  taylpfval  26509  dvntaylp0  26516  ang180lem3  26957  scvxcvx  27131  lgsdir2lem5  27474  ltsres  27807  addsval  28136  mulsval  28283  mulsproplem13  28302  mulsproplem14  28303  oncutlt  28438  n0fincut  28529  zseo  28596  halfcut  28632  z12zsodd  28656  tgbtwnconn1  28825  tgbtwnconn2  28826  tgbtwnconn3  28827  legtrid  28841  hltr  28863  hlbtwn  28864  btwnhl1  28865  btwnhl2  28866  tglineneq  28899  ncolncol  28901  colmid  28946  symquadprlnglem  28951  footexALT  28979  footexlem2  28981  colperpexlem3  28994  colperpex  28995  mideulem2  28996  opphllem  28997  hlpasch  29019  hphl  29034  hlopp  29035  lnincplng  29047  plngrotlem2  29051  symquadmid  29089  hypcgrlem1  29090  hypcgrlem2  29091  trgcopy  29096  trgcopyeulem  29097  cgracgr  29110  cgraswap  29112  cgrahl  29119  cgracol  29120  ragcgra  29127  cgrarag  29128  inagflat  29138  inaghl  29143  prlngref  29171  symquadprlng  29193  colinearalglem4  29240  axcontlem3  29297  edglnl  29474  clwlkclwwlklem2a  30330  clwwlknonmpo  30421  trlsegvdeg  30559  nfrgr2v  30604  frgrwopreg  30655  frgrreg  30726  ex-natded5.7  30743  ex-natded5.13  30747  ex-natded9.20  30749  ex-natded9.20-2  30750  f1ocnt  33126  linds2eq  33675  constrelextdg2  34118  submateqlem2  34179  measxun2  34581  measssd  34586  measiun  34589  meascnbl  34590  carsgclctun  34692  satfvsucsuc  35838  fmlasucdisj  35872  satfun  35884  satfv1fvfmla1  35896  2goelgoanfmla1  35897  outsideoftr  36602  lineunray  36620  weiunpo  36957  knoppndvlem6  37087  topdifinffinlem  37974  areacirclem4  38343  smprngopr  38684  tsbi1  38763  tsbi2  38764  lkrshpor  39862  2atmat0  40281  dochsnkrlem3  42226  dvrelog2b  42814  aks4d1p1  42824  aks6d1c2p2  42867  hashnexinjle  42877  unitscyglem2  42944  pell1234qrdich  43571  acongid  43685  acongtr  43688  acongrep  43690  acongeq  43693  jm2.23  43706  jm2.25  43709  jm2.27a  43715  kelac2lem  43774  mendvscafval  43896  fzunt1d  44166  rp-fakeimass  44221  frege106d  44464  clsk1indlem3  44752  nanorxor  44998  undif3VD  45573  refsum2cnlem1  45740  reclt0d  46085  limciccioolb  46320  limcicciooub  46334  wallispilem3  46764  fourierdlem35  46839  fourierdlem80  46883  fourierswlem  46927  fouriersw  46928  squeezedltsq  47586  dfatprc  47850  nltle2tri  48033  icceuelpartlem  48167  requad01  48369  even3prm2  48467  stgoldbwt  48524  clnbgrvtxel  48577  dfclnbgr6  48604  dfnbgr6  48605  dfsclnbgr6  48606  clnbgrgrim  48682  usgrexmpl2trifr  48785  gpgusgralem  48804  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpg3nbgrvtx0  48824  gpg3nbgrvtx0ALT  48825  gpg3nbgrvtx1  48826  gpg5edgnedg  48878  smprngprmrng  49087  ztprmneprm  49110  altgsumbcALT  49116  zlmodzxznm  49260  zlmodzxzldeplem4  49266  reorelicc  49473  prelrrx2b  49477  rrx2plord1  49484  line2x  49517  itscnhlc0xyqsol  49528  itscnhlinecirc02plem1  49545  fvconst0ci  49652  upfval  49937