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 20806. (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  3012  undif3  3442  disjprg  4035  poxp  6243  unxpwdom2  7318  sornom  7919  fin11a  8025  fin56  8035  fin1a2lem11  8052  axdc3lem2  8093  gchdomtri  8267  0tsk  8393  zmulcl  10082  xrlttri  10489  xmulpnf1  10610  iccsplit  10784  zsum  12207  sumsplit  12247  rpnnen2lem11  12519  sadadd2lem2  12657  vdwlem6  13049  vdwlem10  13053  mreexexlem4d  13565  mreexfidimd  13568  gsummulgz  15231  drngnidl  15997  cnsubrg  16448  fctop  16757  cctop  16759  ppttop  16760  pptbas  16761  pmltpclem2  18825  dvne0  19374  taylplem2  19759  taylpfval  19760  dvntaylp0  19767  ang180lem3  20125  scvxcvx  20296  wilthlem2  20323  lgsdir2lem5  20582  ex-natded5.7  20814  ex-natded5.13  20818  ex-natded9.20  20820  ex-natded9.20-2  20821  measxun2  23553  measssd  23558  measiun  23560  meascnbl  23561  zprod  24160  sltres  24389  nobnddown  24426  colinearalglem4  24609  axcontlem3  24666  outsideoftr  24824  lineunray  24842  areacirclem5  25032  smprngopr  26780  pell1234qrdich  27049  acongid  27165  acongtr  27168  acongrep  27170  acongeq  27173  jm2.23  27192  jm2.25  27195  jm2.27a  27201  kelac2lem  27265  psgnunilem1  27519  refsum2cnlem1  27811  wallispilem3  27919  elfznelfzo  28213  undif3VD  28974  lkrshpor  29919  2atmat0  30337  dochsnkrlem3  32283
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