Theorem orcd 392

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded 23625. (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 385	. 2 |- ( ps -> ( ps \/ ch ) )
3	1, 2	syl 16	1 |- ( ph -> ( ps \/ ch ) )

Syntax hints:   -> wi 4   \/ wo 368

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 185  df-or 370

This theorem is referenced by:  olcd  393  pm2.47  399  orim12i  516  cases2  963  cadan  1433  sbc2or  3210  undif3  3626  rabsnifsb  3958  disjprg  4303  poxp  6699  unxpwdom2  7818  sornom  8461  fin11a  8567  fin56  8577  fin1a2lem11  8594  axdc3lem2  8635  gchdomtri  8811  0tsk  8937  zmulcl  10708  xrlttri  11131  xmulpnf1  11252  iccsplit  11433  elfznelfzo  11645  ccatsymb  12296  zsum  13210  sumsplit  13250  rpnnen2lem11  13522  sadadd2lem2  13661  vdwlem6  14062  vdwlem10  14066  cshwshashlem1  14137  mreexexlem4d  14600  mreexfidimd  14603  symg2bas  15918  psgnunilem1  16014  gsummulgz  16454  srgbinomlem4  16656  drngnidl  17326  cnsubrg  17888  fctop  18623  cctop  18625  ppttop  18626  pptbas  18627  metusttoOLD  20147  metustto  20148  pmltpclem2  20948  dvne0  21498  taylplem2  21844  taylpfval  21845  dvntaylp0  21852  ang180lem3  22222  scvxcvx  22394  wilthlem2  22422  lgsdir2lem5  22681  tgbtwnconn1  23022  tgbtwnconn2  23023  tgbtwnconn3  23024  legtrid  23037  ncolne1  23047  tglineneq  23064  ncolncol  23066  colmid  23097  footex  23124  colinearalglem4  23170  axcontlem3  23227  ex-natded5.7  23633  ex-natded5.13  23637  ex-natded9.20  23639  ex-natded9.20-2  23640  measxun2  26639  measssd  26644  measiun  26647  meascnbl  26648  zprod  27465  sltres  27820  nobnddown  27857  outsideoftr  28175  lineunray  28193  areacirclem4  28506  smprngopr  28871  tsbi1  28963  tsbi2  28964  pell1234qrdich  29221  acongid  29337  acongtr  29340  acongrep  29342  acongeq  29345  jm2.23  29364  jm2.25  29367  jm2.27a  29373  kelac2lem  29436  refsum2cnlem1  29778  wallispilem3  29881  nn0lt2  30205  nn01to3  30206  hashrabsn01  30251  clwlkisclwwlklem2a  30466  frgra2v  30610  frgrawopreg  30661  2spotiundisj  30674  frgrareg  30729  ztprmneprm  30758  altgsumbcALT  30769  lindslinindsimp1  31010  zlmodzxznm  31058  zlmodzxzldeplem4  31064  undif3VD  31637  bj-animorl  32092  bj-animorrl  32095  lkrshpor  32771  2atmat0  33189  dochsnkrlem3  35135