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

Theorem orcd 707
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 686 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-io 683
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  olcd  708  pm2.47  714  orim12i  733  dcor  904  undif3ss  3307  dcun  3443  exmidn0m  4094  exmidsssn  4095  reg2exmidlema  4419  acexmidlem1  5738  poxp  6097  nntri2or2  6362  nnm00  6393  ssfilem  6737  diffitest  6749  tridc  6761  finexdc  6764  fientri3  6771  unsnfidcex  6776  unsnfidcel  6777  fidcenumlemrks  6809  finomni  6980  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  nqprloc  7321  mullocprlem  7346  recexprlemloc  7407  ltxrlt  7798  zmulcl  9075  nn0lt2  9100  zeo  9124  xrltso  9550  apbtwnz  10015  expnegap0  10269  xrmaxadd  10998  zsumdc  11121  fsumsplit  11144  sumsplitdc  11169  isumlessdc  11233  suplociccreex  12698  djulclALT  12935  trilpolemres  13162
  Copyright terms: Public domain W3C validator