Theorem orcd 392

Description: Deduction introducing a disjunct. A translation of natural deduction rule \/ IR ( \/ insertion right), see natded 23545. (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  513  cases2  958  cadan  1438  sbc2or  3192  undif3  3608  rabsnifsb  3940  disjprg  4285  poxp  6683  unxpwdom2  7799  sornom  8442  fin11a  8548  fin56  8558  fin1a2lem11  8575  axdc3lem2  8616  gchdomtri  8792  0tsk  8918  zmulcl  10689  xrlttri  11112  xmulpnf1  11233  iccsplit  11414  elfznelfzo  11626  ccatsymb  12277  zsum  13191  sumsplit  13231  rpnnen2lem11  13503  sadadd2lem2  13642  vdwlem6  14043  vdwlem10  14047  cshwshashlem1  14118  mreexexlem4d  14581  mreexfidimd  14584  symg2bas  15896  psgnunilem1  15992  gsummulgz  16431  srgbinomlem4  16631  drngnidl  17289  cnsubrg  17832  fctop  18567  cctop  18569  ppttop  18570  pptbas  18571  metusttoOLD  20091  metustto  20092  pmltpclem2  20892  dvne0  21442  taylplem2  21788  taylpfval  21789  dvntaylp0  21796  ang180lem3  22166  scvxcvx  22338  wilthlem2  22366  lgsdir2lem5  22625  tgbtwnconn1  22962  tgbtwnconn2  22963  tgbtwnconn3  22964  legtrid  22977  ncolne1  22987  tglineneq  23001  ncolncol  23003  colmid  23031  colinearalglem4  23090  axcontlem3  23147  ex-natded5.7  23553  ex-natded5.13  23557  ex-natded9.20  23559  ex-natded9.20-2  23560  measxun2  26560  measssd  26565  measiun  26568  meascnbl  26569  zprod  27379  sltres  27734  nobnddown  27771  outsideoftr  28089  lineunray  28107  areacirclem4  28412  smprngopr  28777  tsbi1  28869  tsbi2  28870  pell1234qrdich  29127  acongid  29243  acongtr  29246  acongrep  29248  acongeq  29251  jm2.23  29270  jm2.25  29273  jm2.27a  29279  kelac2lem  29342  refsum2cnlem1  29684  wallispilem3  29787  nn0lt2  30111  nn01to3  30112  hashrabsn01  30157  clwlkisclwwlklem2a  30372  frgra2v  30516  frgrawopreg  30567  2spotiundisj  30580  frgrareg  30635  ztprmneprm  30663  altgsumbcALT  30667  lindslinindsimp1  30832  zlmodzxznm  30880  zlmodzxzldeplem4  30886  undif3VD  31452  lkrshpor  32474  2atmat0  32892  dochsnkrlem3  34838