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

Theorem orcd 393
Description: Deduction introducing a disjunct. A translation of natural deduction rule  \/ IR ( \/ insertion right), see natded 25839. (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 386 . 2  |-  ( ps 
->  ( ps  \/  ch ) )
31, 2syl 17 1  |-  ( ph  ->  ( ps  \/  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  olcd  394  pm2.47  400  orim12i  518  cases2  980  cadan  1507  sbc2or  3308  undif3  3734  rabsnifsb  4065  disjprg  4416  poxp  6916  unxpwdom2  8106  sornom  8708  fin11a  8814  fin56  8824  fin1a2lem11  8841  axdc3lem2  8882  gchdomtri  9055  0tsk  9181  zmulcl  10986  nn0lt2  11001  nn01to3  11258  xrlttri  11439  xmulpnf1  11561  iccsplit  11766  elfznelfzo  12014  hashrabsn01  12552  ccatsymb  12720  zsum  13772  sumsplit  13817  zprod  13979  rpnnen2lem11  14265  sadadd2lem2  14412  lcmfunsnlem2lem1  14599  lcmfunsnlem2  14601  vdwlem6  14924  vdwlem10  14928  cshwshashlem1  15054  mreexexlem4d  15541  mreexfidimd  15544  sgrp2nmndlem5  16651  symg2bas  17027  psgnunilem1  17122  gsummulgz  17564  srgbinomlem4  17764  drngnidl  18441  cnsubrg  19016  chfacfscmulgsum  19871  chfacfpmmulgsum  19875  fctop  20006  cctop  20008  ppttop  20009  pptbas  20010  metustto  21555  pmltpclem2  22387  dvne0  22950  taylplem2  23306  taylpfval  23307  dvntaylp0  23314  ang180lem3  23727  scvxcvx  23898  wilthlem2  23981  lgsdir2lem5  24242  tgbtwnconn1  24607  tgbtwnconn2  24608  tgbtwnconn3  24609  legtrid  24623  hltr  24642  hlbtwn  24643  btwnhl1  24644  btwnhl2  24645  tglineneq  24676  ncolncol  24678  colmid  24720  footex  24750  colperpexlem3  24761  colperpex  24762  mideulem2  24763  opphllem  24764  hlpasch  24785  colhp  24799  hphl  24800  hypcgrlem1  24828  hypcgrlem2  24829  trgcopy  24833  trgcopyeulem  24834  cgracgr  24847  cgraswap  24849  cgrahl  24855  cgracol  24856  inaghl  24868  colinearalglem4  24926  axcontlem3  24983  clwlkisclwwlklem2a  25499  frgra2v  25713  frgrawopreg  25763  2spotiundisj  25776  frgrareg  25831  ex-natded5.7  25847  ex-natded5.13  25851  ex-natded9.20  25853  ex-natded9.20-2  25854  padct  28301  f1ocnt  28370  submateqlem2  28630  measxun2  29028  measssd  29033  measiun  29036  meascnbl  29037  carsgclctun  29149  sltres  30546  nobnddown  30583  outsideoftr  30889  lineunray  30907  bj-animorl  31138  bj-animorrl  31141  topdifinffinlem  31691  areacirclem4  31949  smprngopr  32199  tsbi1  32289  tsbi2  32290  lkrshpor  32592  2atmat0  33010  dochsnkrlem3  34958  pell1234qrdich  35627  acongid  35745  acongtr  35748  acongrep  35750  acongeq  35753  jm2.23  35771  jm2.25  35774  jm2.27a  35780  kelac2lem  35842  rp-fakeimass  36076  frege106d  36207  nanorxor  36511  undif3VD  37140  refsum2cnlem1  37219  limciccioolb  37521  limcicciooub  37537  wallispilem3  37749  fourierdlem35  37825  fourierdlem80  37870  fourierswlem  37914  fouriersw  37915  nltle2tri  38428  icceuelpartlem  38461  stgoldbwt  38589  n0snor2el  38701  propeqop  38704  nrhmzr  39145  ztprmneprm  39402  altgsumbcALT  39408  lindslinindsimp1  39524  zlmodzxznm  39564  zlmodzxzldeplem4  39570
  Copyright terms: Public domain W3C validator