Theorem orcd 394

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded 25853. (Contributed by NM, 20-Sep-2007.)

Hypothesis

Ref	Expression
orcd.1	|- ( ph -> ps )

Assertion

Ref	Expression
orcd	|- ( ph -> ( ps \/ ch ) )

Proof of Theorem orcd

Step	Hyp	Ref	Expression
1		orcd.1	. 2 |- ( ph -> ps )
2		orc 387	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 17	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -> wi 4   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  olcd  395  pm2.47  401  orim12i  519  cases2  983  cadan  1512  sbc2or  3276  undif3  3704  rabsnifsb  4040  disjprg  4398  poxp  6908  unxpwdom2  8103  sornom  8707  fin11a  8813  fin56  8823  fin1a2lem11  8840  axdc3lem2  8881  gchdomtri  9054  0tsk  9180  zmulcl  10985  nn0lt2  11000  nn01to3  11257  xrlttri  11438  xmulpnf1  11560  iccsplit  11765  elfznelfzo  12014  hashrabsn01  12552  ccatsymb  12727  zsum  13784  sumsplit  13829  zprod  13991  rpnnen2lem11  14277  sadadd2lem2  14424  lcmfunsnlem2lem1  14611  lcmfunsnlem2  14613  vdwlem6  14936  vdwlem10  14940  cshwshashlem1  15066  mreexexlem4d  15553  mreexfidimd  15556  sgrp2nmndlem5  16663  symg2bas  17039  psgnunilem1  17134  gsummulgz  17576  srgbinomlem4  17776  drngnidl  18453  cnsubrg  19028  chfacfscmulgsum  19884  chfacfpmmulgsum  19888  fctop  20019  cctop  20021  ppttop  20022  pptbas  20023  metustto  21568  pmltpclem2  22400  dvne0  22963  taylplem2  23319  taylpfval  23320  dvntaylp0  23327  ang180lem3  23740  scvxcvx  23911  wilthlem2  23994  lgsdir2lem5  24255  tgbtwnconn1  24620  tgbtwnconn2  24621  tgbtwnconn3  24622  legtrid  24636  hltr  24655  hlbtwn  24656  btwnhl1  24657  btwnhl2  24658  tglineneq  24689  ncolncol  24691  colmid  24733  footex  24763  colperpexlem3  24774  colperpex  24775  mideulem2  24776  opphllem  24777  hlpasch  24798  colhp  24812  hphl  24813  hypcgrlem1  24841  hypcgrlem2  24842  trgcopy  24846  trgcopyeulem  24847  cgracgr  24860  cgraswap  24862  cgrahl  24868  cgracol  24869  inaghl  24881  colinearalglem4  24939  axcontlem3  24996  clwlkisclwwlklem2a  25513  frgra2v  25727  frgrawopreg  25777  2spotiundisj  25790  frgrareg  25845  ex-natded5.7  25861  ex-natded5.13  25865  ex-natded9.20  25867  ex-natded9.20-2  25868  padct  28307  f1ocnt  28376  submateqlem2  28634  measxun2  29032  measssd  29037  measiun  29040  meascnbl  29041  carsgclctun  29153  sltres  30551  nobnddown  30590  outsideoftr  30896  lineunray  30914  bj-animorl  31145  bj-animorrl  31148  topdifinffinlem  31750  areacirclem4  32035  smprngopr  32285  tsbi1  32375  tsbi2  32376  lkrshpor  32673  2atmat0  33091  dochsnkrlem3  35039  pell1234qrdich  35707  acongid  35825  acongtr  35828  acongrep  35830  acongeq  35833  jm2.23  35851  jm2.25  35854  jm2.27a  35860  kelac2lem  35922  rp-fakeimass  36156  frege106d  36347  nanorxor  36653  undif3VD  37279  refsum2cnlem1  37358  limciccioolb  37701  limcicciooub  37717  wallispilem3  37929  fourierdlem35  38005  fourierdlem80  38050  fourierswlem  38094  fouriersw  38095  nltle2tri  38716  icceuelpartlem  38749  stgoldbwt  38877  n0snor2el  38996  propeqop  38999  nrhmzr  39926  ztprmneprm  40181  altgsumbcALT  40187  lindslinindsimp1  40303  zlmodzxznm  40343  zlmodzxzldeplem4  40349