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

Theorem orcd 383
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IR ( \/ insertion right), see natded 21712. (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 376 . 2  |-  ( ps 
->  ( ps  \/  ch ) )
31, 2syl 16 1  |-  ( ph  ->  ( ps  \/  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359
This theorem is referenced by:  olcd  384  pm2.47  390  orim12i  504  sbc2or  3170  undif3  3603  rabrsn  3875  disjprg  4209  poxp  6459  unxpwdom2  7557  sornom  8158  fin11a  8264  fin56  8274  fin1a2lem11  8291  axdc3lem2  8332  gchdomtri  8505  0tsk  8631  zmulcl  10325  xrlttri  10733  xmulpnf1  10854  iccsplit  11030  elfznelfzo  11193  zsum  12513  sumsplit  12553  rpnnen2lem11  12825  sadadd2lem2  12963  vdwlem6  13355  vdwlem10  13359  mreexexlem4d  13873  mreexfidimd  13876  gsummulgz  15539  drngnidl  16301  cnsubrg  16760  fctop  17069  cctop  17071  ppttop  17072  pptbas  17073  metusttoOLD  18588  metustto  18589  pmltpclem2  19347  dvne0  19896  taylplem2  20281  taylpfval  20282  dvntaylp0  20289  ang180lem3  20654  scvxcvx  20825  wilthlem2  20853  lgsdir2lem5  21112  ex-natded5.7  21720  ex-natded5.13  21724  ex-natded9.20  21726  ex-natded9.20-2  21727  measxun2  24565  measssd  24570  measiun  24573  meascnbl  24574  sibfof  24655  zprod  25264  sltres  25620  nobnddown  25657  colinearalglem4  25849  axcontlem3  25906  outsideoftr  26064  lineunray  26082  areacirclem4  26296  smprngopr  26663  pell1234qrdich  26925  acongid  27041  acongtr  27044  acongrep  27046  acongeq  27049  jm2.23  27068  jm2.25  27071  jm2.27a  27077  kelac2lem  27140  psgnunilem1  27394  refsum2cnlem1  27685  wallispilem3  27793  ccatsymb  28180  cshwssizelem2  28282  frgrawopreg  28439  2spotiundisj  28452  undif3VD  28995  lkrshpor  29906  2atmat0  30324  dochsnkrlem3  32270
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 179  df-or 361
  Copyright terms: Public domain W3C validator