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

Theorem orcd 406
 Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 27390. (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 399 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382 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 384 This theorem is referenced by:  olcd  407  pm2.47  413  animorl  504  animorrl  507  orim12i  537  cases2ALT  1017  sbc2or  3477  undif3OLD  3922  rabsnifsb  4289  n0snor2el  4396  disjprg  4680  propeqop  4999  poxp  7334  unxpwdom2  8534  sornom  9137  fin11a  9243  fin56  9253  fin1a2lem11  9270  axdc3lem2  9311  gchdomtri  9489  0tsk  9615  zmulcl  11464  nn0lt2  11478  nn01to3  11819  xrlttri  12010  xmulpnf1  12142  iccsplit  12343  elfznelfzo  12613  hashrabsn01  13200  hashsn01  13242  ccatsymb  13400  zsum  14493  sumsplit  14543  zprod  14711  rpnnen2lem11  14997  sadadd2lem2  15219  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  vdwlem6  15737  vdwlem10  15741  cshwshashlem1  15849  basprssdmsets  15972  mreexexlem4d  16354  mreexfidimd  16358  sgrp2nmndlem5  17463  symg2bas  17864  psgnunilem1  17959  gsummulgz  18389  srgbinomlem4  18589  drngnidl  19277  cnsubrg  19854  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  fctop  20856  cctop  20858  ppttop  20859  pptbas  20860  metustto  22405  pmltpclem2  23264  dvne0  23819  taylplem2  24163  taylpfval  24164  dvntaylp0  24171  ang180lem3  24586  scvxcvx  24757  wilthlem2  24840  lgsdir2lem5  25099  tgbtwnconn1  25515  tgbtwnconn2  25516  tgbtwnconn3  25517  legtrid  25531  hltr  25550  hlbtwn  25551  btwnhl1  25552  btwnhl2  25553  tglineneq  25584  ncolncol  25586  colmid  25628  footex  25658  colperpexlem3  25669  colperpex  25670  mideulem2  25671  opphllem  25672  hlpasch  25693  colhp  25707  hphl  25708  hypcgrlem1  25736  hypcgrlem2  25737  trgcopy  25741  trgcopyeulem  25742  cgracgr  25755  cgraswap  25757  cgrahl  25763  cgracol  25764  inaghl  25776  colinearalglem4  25834  axcontlem3  25891  edglnl  26083  clwlkclwwlklem2a  26964  trlsegvdeg  27205  nfrgr2v  27252  frgrwopreg  27303  frgrreg  27381  ex-natded5.7  27398  ex-natded5.13  27402  ex-natded9.20  27404  ex-natded9.20-2  27405  padct  29625  f1ocnt  29687  submateqlem2  30002  measxun2  30401  measssd  30406  measiun  30409  meascnbl  30410  carsgclctun  30511  sltres  31940  outsideoftr  32361  lineunray  32379  knoppndvlem6  32633  topdifinffinlem  33325  areacirclem4  33633  smprngopr  33981  tsbi1  34070  tsbi2  34071  lkrshpor  34712  2atmat0  35130  dochsnkrlem3  37077  pell1234qrdich  37742  acongid  37859  acongtr  37862  acongrep  37864  acongeq  37867  jm2.23  37880  jm2.25  37883  jm2.27a  37889  kelac2lem  37951  rp-fakeimass  38174  frege106d  38364  clsk1indlem3  38658  nanorxor  38821  undif3VD  39432  refsum2cnlem1  39510  reclt0d  39920  limciccioolb  40171  limcicciooub  40187  wallispilem3  40602  fourierdlem35  40677  fourierdlem80  40721  fourierswlem  40765  fouriersw  40766  nltle2tri  41648  icceuelpartlem  41696  even3prm2  41953  stgoldbwt  41989  nrhmzr  42198  ztprmneprm  42450  altgsumbcALT  42456  lindslinindsimp1  42571  zlmodzxznm  42611  zlmodzxzldeplem4  42617
 Copyright terms: Public domain W3C validator