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

Theorem orcd 407
Description: Deduction introducing a disjunct. A translation of natural deduction rule IR ( insertion right), see natded 27244. (Contributed by NM, 20-Sep-2007.)
Hypothesis
Ref Expression
orcd.1 (𝜑𝜓)
Assertion
Ref Expression
orcd (𝜑 → (𝜓𝜒))

Proof of Theorem orcd
StepHypRef Expression
1 orcd.1 . 2 (𝜑𝜓)
2 orc 400 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  olcd  408  pm2.47  414  animorl  505  animorrl  508  orim12i  538  cases2  993  sbc2or  3442  undif3OLD  3887  rabsnifsb  4255  n0snor2el  4362  disjprg  4646  propeqop  4968  poxp  7286  unxpwdom2  8490  sornom  9096  fin11a  9202  fin56  9212  fin1a2lem11  9229  axdc3lem2  9270  gchdomtri  9448  0tsk  9574  zmulcl  11423  nn0lt2  11437  nn01to3  11778  xrlttri  11969  xmulpnf1  12101  iccsplit  12302  elfznelfzo  12569  hashrabsn01  13157  hashsn01  13199  ccatsymb  13361  zsum  14443  sumsplit  14493  zprod  14661  rpnnen2lem11  14947  sadadd2lem2  15166  lcmfunsnlem2lem1  15345  lcmfunsnlem2  15347  vdwlem6  15684  vdwlem10  15688  cshwshashlem1  15796  basprssdmsets  15919  mreexexlem4d  16301  mreexfidimd  16305  sgrp2nmndlem5  17410  symg2bas  17812  psgnunilem1  17907  gsummulgz  18337  srgbinomlem4  18537  drngnidl  19223  cnsubrg  19800  chfacfscmulgsum  20659  chfacfpmmulgsum  20663  fctop  20802  cctop  20804  ppttop  20805  pptbas  20806  metustto  22352  pmltpclem2  23212  dvne0  23768  taylplem2  24112  taylpfval  24113  dvntaylp0  24120  ang180lem3  24535  scvxcvx  24706  wilthlem2  24789  lgsdir2lem5  25048  tgbtwnconn1  25464  tgbtwnconn2  25465  tgbtwnconn3  25466  legtrid  25480  hltr  25499  hlbtwn  25500  btwnhl1  25501  btwnhl2  25502  tglineneq  25533  ncolncol  25535  colmid  25577  footex  25607  colperpexlem3  25618  colperpex  25619  mideulem2  25620  opphllem  25621  hlpasch  25642  colhp  25656  hphl  25657  hypcgrlem1  25685  hypcgrlem2  25686  trgcopy  25690  trgcopyeulem  25691  cgracgr  25704  cgraswap  25706  cgrahl  25712  cgracol  25713  inaghl  25725  colinearalglem4  25783  axcontlem3  25840  edglnl  26032  clwlkclwwlklem2a  26893  trlsegvdeg  27080  nfrgr2v  27129  frgrwopreg  27172  frgrreg  27236  ex-natded5.7  27252  ex-natded5.13  27256  ex-natded9.20  27258  ex-natded9.20-2  27259  padct  29482  f1ocnt  29544  submateqlem2  29859  measxun2  30258  measssd  30263  measiun  30266  meascnbl  30267  carsgclctun  30368  sltres  31799  outsideoftr  32220  lineunray  32238  knoppndvlem6  32492  topdifinffinlem  33175  areacirclem4  33483  smprngopr  33831  tsbi1  33920  tsbi2  33921  lkrshpor  34220  2atmat0  34638  dochsnkrlem3  36586  pell1234qrdich  37251  acongid  37368  acongtr  37371  acongrep  37373  acongeq  37376  jm2.23  37389  jm2.25  37392  jm2.27a  37398  kelac2lem  37460  rp-fakeimass  37683  frege106d  37873  clsk1indlem3  38167  nanorxor  38330  undif3VD  38944  refsum2cnlem1  39022  reclt0d  39426  limciccioolb  39659  limcicciooub  39675  wallispilem3  40053  fourierdlem35  40128  fourierdlem80  40172  fourierswlem  40216  fouriersw  40217  nltle2tri  41092  icceuelpartlem  41141  even3prm2  41399  stgoldbwt  41435  nrhmzr  41644  ztprmneprm  41896  altgsumbcALT  41902  lindslinindsimp1  42017  zlmodzxznm  42057  zlmodzxzldeplem4  42063
  Copyright terms: Public domain W3C validator