Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  orcd GIF version

Theorem orcd 723
 Description: Deduction introducing a disjunct. (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 702 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∨ wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  olcd  724  pm2.47  730  orim12i  749  dcor  920  undif3ss  3344  dcun  3480  exmidn0m  4135  exmidsssn  4136  reg2exmidlema  4460  acexmidlem1  5782  poxp  6141  nntri2or2  6406  nnm00  6437  ssfilem  6781  diffitest  6793  tridc  6805  finexdc  6808  fientri3  6820  unsnfidcex  6825  unsnfidcel  6826  fidcenumlemrks  6858  finomni  7033  exmidfodomrlemeldju  7084  exmidfodomrlemreseldju  7085  exmidfodomrlemr  7087  exmidfodomrlemrALT  7088  exmidaclem  7093  nqprloc  7406  mullocprlem  7431  recexprlemloc  7492  ltxrlt  7883  zmulcl  9160  nn0lt2  9185  zeo  9209  xrltso  9641  apbtwnz  10107  expnegap0  10361  xrmaxadd  11091  zsumdc  11214  fsumsplit  11237  sumsplitdc  11262  isumlessdc  11326  zproddc  11409  suplociccreex  12846  djulclALT  13218  trilpolemres  13456  trirec0  13458  nconstwlpolem0  13476  nconstwlpolem  13478
 Copyright terms: Public domain W3C validator