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

Theorem orcd 870
 Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 28198. (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 864 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  olcd  871  pm2.47  881  orim12i  906  animorl  975  animorrl  978  cases2ALT  1044  sbc2or  3729  rabsnifsb  4618  n0snor2el  4724  disjprgw  5026  disjprg  5027  propeqop  5363  nf1oconst  7040  poxp  7808  unxpwdom2  9039  djuunxp  9337  sornom  9691  fin11a  9797  fin56  9807  fin1a2lem11  9824  axdc3lem2  9865  gchdomtri  10043  0tsk  10169  zmulcl  12022  nn0lt2  12036  nn01to3  12332  xrlttri  12523  xmulpnf1  12658  iccsplit  12866  elfznelfzo  13140  hashrabsn01  13733  hashsn01  13776  swrdnnn0nd  14012  zsum  15070  sumsplit  15118  zprod  15286  rpnnen2lem11  15572  lcmfunsnlem2lem1  15975  lcmfunsnlem2  15977  vdwlem6  16315  vdwlem10  16319  cshwshashlem1  16424  basprssdmsets  16544  mreexfidimd  16916  smndex1mgm  18067  sgrp2nmndlem5  18089  symg2bas  18517  psgnunilem1  18617  oppglsm  18763  gsummulgz  19060  prmgrpsimpgd  19233  srgbinomlem4  19290  dvrfval  19434  cnsubrg  20155  marrepfval  21175  marepvfval  21180  chfacfscmulgsum  21475  chfacfpmmulgsum  21479  fctop  21619  cctop  21621  pptbas  21623  metustto  23170  pmltpclem2  24063  dvne0  24624  taylplem2  24969  taylpfval  24970  dvntaylp0  24977  ang180lem3  25407  scvxcvx  25581  lgsdir2lem5  25923  tgbtwnconn1  26379  tgbtwnconn2  26380  tgbtwnconn3  26381  legtrid  26395  hltr  26414  hlbtwn  26415  btwnhl1  26416  btwnhl2  26417  tglineneq  26448  ncolncol  26450  colmid  26492  footexALT  26522  footexlem2  26524  colperpexlem3  26536  colperpex  26537  mideulem2  26538  opphllem  26539  hlpasch  26560  hphl  26575  hypcgrlem1  26603  hypcgrlem2  26604  trgcopy  26608  trgcopyeulem  26609  cgracgr  26622  cgraswap  26624  cgrahl  26631  cgracol  26632  inagflat  26644  inaghl  26649  colinearalglem4  26713  axcontlem3  26770  edglnl  26946  clwlkclwwlklem2a  27793  clwwlknonmpo  27884  trlsegvdeg  28022  nfrgr2v  28067  frgrwopreg  28118  frgrreg  28189  ex-natded5.7  28206  ex-natded5.13  28210  ex-natded9.20  28212  ex-natded9.20-2  28213  padct  30491  f1ocnt  30561  linds2eq  31005  submateqlem2  31176  measxun2  31594  measssd  31599  measiun  31602  meascnbl  31603  carsgclctun  31704  satfvsucsuc  32740  fmlasucdisj  32774  satfun  32786  satfv1fvfmla1  32798  2goelgoanfmla1  32799  sltres  33297  outsideoftr  33718  lineunray  33736  knoppndvlem6  33984  topdifinffinlem  34783  areacirclem4  35167  smprngopr  35509  tsbi1  35590  tsbi2  35591  lkrshpor  36422  2atmat0  36841  dochsnkrlem3  38786  pell1234qrdich  39845  acongid  39959  acongtr  39962  acongrep  39964  acongeq  39967  jm2.23  39980  jm2.25  39983  jm2.27a  39989  kelac2lem  40051  mendvscafval  40177  rp-fakeimass  40263  frege106d  40499  clsk1indlem3  40789  nanorxor  41052  undif3VD  41631  refsum2cnlem1  41709  reclt0d  42065  limciccioolb  42306  limcicciooub  42322  wallispilem3  42752  fourierdlem35  42827  fourierdlem80  42871  fourierswlem  42915  fouriersw  42916  dfatprc  43729  nltle2tri  43913  icceuelpartlem  43995  requad01  44182  even3prm2  44280  stgoldbwt  44337  isomuspgrlem1  44388  nrhmzr  44540  ztprmneprm  44792  altgsumbcALT  44798  zlmodzxznm  44947  zlmodzxzldeplem4  44953  reorelicc  45165  prelrrx2b  45169  rrx2plord1  45176  line2x  45209  itscnhlc0xyqsol  45220  itscnhlinecirc02plem1  45237
 Copyright terms: Public domain W3C validator