MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcd Unicode version

Theorem orcd 381
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IR ( \/ insertion right), see natded 20790. (Contributed by NM, 20-Sep-2007.)
Hypothesis
Ref Expression
orcd.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
orcd  |-  ( ph  ->  ( ps  \/  ch ) )

Proof of Theorem orcd
StepHypRef Expression
1 orcd.1 . 2  |-  ( ph  ->  ps )
2 orc 374 . 2  |-  ( ps 
->  ( ps  \/  ch ) )
31, 2syl 15 1  |-  ( ph  ->  ( ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  olcd  382  pm2.47  388  orim12i  502  sbc2or  2999  undif3  3429  disjprg  4019  poxp  6227  unxpwdom2  7302  sornom  7903  fin11a  8009  fin56  8019  fin1a2lem11  8036  axdc3lem2  8077  gchdomtri  8251  0tsk  8377  zmulcl  10066  xrlttri  10473  xmulpnf1  10594  iccsplit  10768  zsum  12191  sumsplit  12231  rpnnen2lem11  12503  sadadd2lem2  12641  vdwlem6  13033  vdwlem10  13037  mreexexlem4d  13549  mreexfidimd  13552  gsummulgz  15215  drngnidl  15981  cnsubrg  16432  fctop  16741  cctop  16743  ppttop  16744  pptbas  16745  pmltpclem2  18809  dvne0  19358  taylplem2  19743  taylpfval  19744  dvntaylp0  19751  ang180lem3  20109  scvxcvx  20280  wilthlem2  20307  lgsdir2lem5  20566  ex-natded5.7  20798  ex-natded5.13  20802  ex-natded9.20  20804  ex-natded9.20-2  20805  measxun2  23538  measssd  23543  measiun  23545  meascnbl  23546  sltres  24318  nobnddown  24355  colinearalglem4  24537  axcontlem3  24594  outsideoftr  24752  lineunray  24770  areacirclem5  24929  smprngopr  26677  pell1234qrdich  26946  acongid  27062  acongtr  27065  acongrep  27067  acongeq  27070  jm2.23  27089  jm2.25  27092  jm2.27a  27098  kelac2lem  27162  psgnunilem1  27416  refsum2cnlem1  27708  wallispilem3  27816  undif3VD  28658  lkrshpor  29297  2atmat0  29715  dochsnkrlem3  31661
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator