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

Theorem orcd 685
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 666 . 2 (𝜓 → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  olcd  686  pm2.47  692  orim12i  709  dcor  877  undif3ss  3241  reg2exmidlema  4305  acexmidlem1  5559  poxp  5904  nntri2or2  6162  nnm00  6189  ssfilem  6431  diffitest  6443  fientri3  6459  unsnfidcex  6464  unsnfidcel  6465  nqprloc  6849  mullocprlem  6874  recexprlemloc  6935  ltxrlt  7297  zmulcl  8537  nn0lt2  8562  zeo  8585  xrltso  8999  apbtwnz  9408  expnegap0  9633
  Copyright terms: Public domain W3C validator