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

Theorem orcd 872
Description: Deduction introducing a disjunct. A translation of natural deduction rule IR ( insertion right), see natded 29389. (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 866 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 206  df-or 847
This theorem is referenced by:  olcd  873  pm2.47  883  orim12i  908  animorl  977  animorrl  980  cases2ALT  1048  sbc2or  3753  rabsnifsb  4688  n0snor2el  4796  disjprgw  5105  disjprg  5106  propeqop  5469  nf1oconst  7256  poxp  8065  xpord2indlem  8084  naddcllem  8627  unxpwdom2  9531  djuunxp  9864  sornom  10220  fin11a  10326  fin56  10336  fin1a2lem11  10353  axdc3lem2  10394  gchdomtri  10572  0tsk  10698  zmulcl  12559  nn0lt2  12573  nn01to3  12873  xrlttri  13065  xmulpnf1  13200  iccsplit  13409  elfznelfzo  13684  hashrabsn01  14280  hashsn01  14323  swrdnnn0nd  14551  zsum  15610  sumsplit  15660  zprod  15827  rpnnen2lem11  16113  lcmfunsnlem2lem1  16521  lcmfunsnlem2  16523  vdwlem6  16865  vdwlem10  16869  cshwshashlem1  16975  basprssdmsets  17103  mreexfidimd  17537  smndex1mgm  18724  sgrp2nmndlem5  18746  symg2bas  19181  psgnunilem1  19282  oppglsm  19431  gsummulgz  19727  prmgrpsimpgd  19900  srgbinomlem4  19967  dvrfval  20120  cnsubrg  20873  marrepfval  21925  marepvfval  21930  chfacfscmulgsum  22225  chfacfpmmulgsum  22229  fctop  22370  cctop  22372  pptbas  22374  metustto  23925  pmltpclem2  24829  dvne0  25391  taylplem2  25739  taylpfval  25740  dvntaylp0  25747  ang180lem3  26177  scvxcvx  26351  lgsdir2lem5  26693  sltres  27026  addsval  27296  mulsval  27396  tgbtwnconn1  27559  tgbtwnconn2  27560  tgbtwnconn3  27561  legtrid  27575  hltr  27594  hlbtwn  27595  btwnhl1  27596  btwnhl2  27597  tglineneq  27628  ncolncol  27630  colmid  27672  footexALT  27702  footexlem2  27704  colperpexlem3  27716  colperpex  27717  mideulem2  27718  opphllem  27719  hlpasch  27740  hphl  27755  hypcgrlem1  27783  hypcgrlem2  27784  trgcopy  27788  trgcopyeulem  27789  cgracgr  27802  cgraswap  27804  cgrahl  27811  cgracol  27812  inagflat  27824  inaghl  27829  colinearalglem4  27900  axcontlem3  27957  edglnl  28136  clwlkclwwlklem2a  28984  clwwlknonmpo  29075  trlsegvdeg  29213  nfrgr2v  29258  frgrwopreg  29309  frgrreg  29380  ex-natded5.7  29397  ex-natded5.13  29401  ex-natded9.20  29403  ex-natded9.20-2  29404  padct  31678  f1ocnt  31747  linds2eq  32208  submateqlem2  32429  measxun2  32849  measssd  32854  measiun  32857  meascnbl  32858  carsgclctun  32961  satfvsucsuc  33999  fmlasucdisj  34033  satfun  34045  satfv1fvfmla1  34057  2goelgoanfmla1  34058  outsideoftr  34743  lineunray  34761  knoppndvlem6  35009  topdifinffinlem  35847  areacirclem4  36198  smprngopr  36540  tsbi1  36621  tsbi2  36622  lkrshpor  37598  2atmat0  38018  dochsnkrlem3  39963  dvrelog2b  40552  aks4d1p1  40562  aks6d1c2p2  40578  pell1234qrdich  41213  acongid  41328  acongtr  41331  acongrep  41333  acongeq  41336  jm2.23  41349  jm2.25  41352  jm2.27a  41358  kelac2lem  41420  mendvscafval  41546  fzunt1d  41803  rp-fakeimass  41858  frege106d  42101  clsk1indlem3  42389  nanorxor  42659  undif3VD  43238  refsum2cnlem1  43316  reclt0d  43695  limciccioolb  43936  limcicciooub  43952  wallispilem3  44382  fourierdlem35  44457  fourierdlem80  44501  fourierswlem  44545  fouriersw  44546  dfatprc  45436  nltle2tri  45619  icceuelpartlem  45701  requad01  45887  even3prm2  45985  stgoldbwt  46042  isomuspgrlem1  46093  nrhmzr  46245  ztprmneprm  46497  altgsumbcALT  46503  zlmodzxznm  46652  zlmodzxzldeplem4  46658  reorelicc  46870  prelrrx2b  46874  rrx2plord1  46881  line2x  46914  itscnhlc0xyqsol  46925  itscnhlinecirc02plem1  46942  fvconst0ci  46999
  Copyright terms: Public domain W3C validator