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

Theorem orcd 853
 Description: Deduction introducing a disjunct. A translation of natural deduction rule ∨ IR (∨ insertion right), see natded 27596. (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 847 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 826 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 827 This theorem is referenced by:  olcd  854  orim12i  874  pm2.47  901  animorl  906  animorrl  909  cases2ALT  1033  sbc2or  3594  rabsnifsb  4391  n0snor2el  4495  disjprg  4780  propeqop  5100  poxp  7439  unxpwdom2  8648  djuunxp  8946  sornom  9300  fin11a  9406  fin56  9416  fin1a2lem11  9433  axdc3lem2  9474  gchdomtri  9652  0tsk  9778  zmulcl  11627  nn0lt2  11641  nn01to3  11983  xrlttri  12176  xmulpnf1  12308  iccsplit  12511  elfznelfzo  12780  hashrabsn01  13363  hashsn01  13405  ccatsymb  13563  zsum  14656  sumsplit  14706  zprod  14873  rpnnen2lem11  15158  sadadd2lem2  15379  lcmfunsnlem2lem1  15558  lcmfunsnlem2  15560  vdwlem6  15896  vdwlem10  15900  cshwshashlem1  16008  basprssdmsets  16131  mreexexlem4d  16514  mreexfidimd  16517  sgrp2nmndlem5  17623  symg2bas  18024  psgnunilem1  18119  gsummulgz  18549  srgbinomlem4  18750  drngnidl  19443  cnsubrg  20020  chfacfscmulgsum  20884  chfacfpmmulgsum  20888  fctop  21028  cctop  21030  ppttop  21031  pptbas  21032  metustto  22577  pmltpclem2  23436  dvne0  23993  taylplem2  24337  taylpfval  24338  dvntaylp0  24345  ang180lem3  24761  scvxcvx  24932  wilthlem2  25015  lgsdir2lem5  25274  tgbtwnconn1  25690  tgbtwnconn2  25691  tgbtwnconn3  25692  legtrid  25706  hltr  25725  hlbtwn  25726  btwnhl1  25727  btwnhl2  25728  tglineneq  25759  ncolncol  25761  colmid  25803  footex  25833  colperpexlem3  25844  colperpex  25845  mideulem2  25846  opphllem  25847  hlpasch  25868  colhp  25882  hphl  25883  hypcgrlem1  25911  hypcgrlem2  25912  trgcopy  25916  trgcopyeulem  25917  cgracgr  25930  cgraswap  25932  cgrahl  25938  cgracol  25939  inaghl  25951  colinearalglem4  26009  axcontlem3  26066  edglnl  26259  clwlkclwwlklem2a  27145  trlsegvdeg  27404  nfrgr2v  27451  frgrwopreg  27502  frgrreg  27587  ex-natded5.7  27604  ex-natded5.13  27608  ex-natded9.20  27610  ex-natded9.20-2  27611  padct  29831  f1ocnt  29893  submateqlem2  30208  measxun2  30607  measssd  30612  measiun  30615  meascnbl  30616  carsgclctun  30717  sltres  32146  outsideoftr  32567  lineunray  32585  knoppndvlem6  32839  topdifinffinlem  33525  areacirclem4  33828  smprngopr  34176  tsbi1  34265  tsbi2  34266  lkrshpor  34909  2atmat0  35327  dochsnkrlem3  37274  pell1234qrdich  37944  acongid  38061  acongtr  38064  acongrep  38066  acongeq  38069  jm2.23  38082  jm2.25  38085  jm2.27a  38091  kelac2lem  38153  rp-fakeimass  38376  frege106d  38566  clsk1indlem3  38860  nanorxor  39023  undif3VD  39634  refsum2cnlem1  39712  reclt0d  40117  limciccioolb  40365  limcicciooub  40381  wallispilem3  40795  fourierdlem35  40870  fourierdlem80  40914  fourierswlem  40958  fouriersw  40959  nltle2tri  41841  icceuelpartlem  41889  even3prm2  42146  stgoldbwt  42182  nrhmzr  42391  ztprmneprm  42643  altgsumbcALT  42649  lindslinindsimp1  42764  zlmodzxznm  42804  zlmodzxzldeplem4  42810
 Copyright terms: Public domain W3C validator