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

Theorem olcd 706
Description: Deduction introducing a disjunct. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
Hypothesis
Ref Expression
orcd.1 (𝜑𝜓)
Assertion
Ref Expression
olcd (𝜑 → (𝜒𝜓))

Proof of Theorem olcd
StepHypRef Expression
1 orcd.1 . . 3 (𝜑𝜓)
21orcd 705 . 2 (𝜑 → (𝜓𝜒))
32orcomd 701 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wo 680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm2.48  713  pm2.49  714  orim12i  731  pm1.5  737  dcan  901  dcor  902  dcun  3441  exmidn0m  4092  regexmidlem1  4416  reg2exmidlema  4417  nn0suc  4486  nndceq0  4499  acexmidlem1  5736  nntri3or  6355  nntri2or2  6360  nndceq  6361  nndcel  6362  nnm00  6391  ssfilem  6735  diffitest  6747  tridc  6759  finexdc  6762  fientri3  6769  unsnfidcex  6774  unsnfidcel  6775  fidcenumlemrks  6807  fidcenumlemrk  6808  finomni  6978  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  mullocprlem  7342  recexprlemloc  7403  gt0ap0  8351  ltap  8357  recexaplem2  8373  nn1m1nn  8695  nn1gt1  8711  ltpnf  9507  mnflt  9509  xrltso  9522  xrpnfdc  9565  xrmnfdc  9566  exfzdc  9957  apbtwnz  9987  expnnval  10236  exp0  10237  bc0k  10442  bcpasc  10452  xrmaxadd  10970  sumdc  11067  zsumdc  11093  fsum3  11096  fisumss  11101  isumss2  11102  fsumsplit  11116  infssuzex  11538  ctiunctlemudc  11845  suplociccreex  12666  djurclALT  12820  bj-nn0suc0  12959  trilpolemres  13046
  Copyright terms: Public domain W3C validator