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

Theorem orcd 652
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 633 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-io 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  olcd  653  pm2.47  659  orim12i  676  dcor  843  sspsstrir  3046  undif3ss  3198  reg2exmidlema  4259  acexmidlem1  5508  poxp  5853  nntri2or2  6076  nnm00  6102  ssfiexmid  6336  diffitest  6344  fientri3  6353  nqprloc  6643  mullocprlem  6668  recexprlemloc  6729  ltxrlt  7085  zmulcl  8297  nn0lt2  8322  zeo  8343  xrltso  8717  expnegap0  9263
  Copyright terms: Public domain W3C validator