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

Theorem olcd 724
 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 723 . 2 (𝜑 → (𝜓𝜒))
32orcomd 719 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-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm2.48  731  pm2.49  732  orim12i  749  pm1.5  755  dcan  919  dcor  920  dcun  3479  exmidn0m  4133  regexmidlem1  4457  reg2exmidlema  4458  nn0suc  4527  nndceq0  4540  acexmidlem1  5779  nntri3or  6398  nntri2or2  6403  nndceq  6404  nndcel  6405  nnm00  6434  ssfilem  6778  diffitest  6790  tridc  6802  finexdc  6805  fientri3  6813  unsnfidcex  6818  unsnfidcel  6819  fidcenumlemrks  6851  fidcenumlemrk  6852  finomni  7022  exmidfodomrlemeldju  7075  exmidfodomrlemreseldju  7076  exmidfodomrlemr  7078  exmidfodomrlemrALT  7079  exmidaclem  7084  mullocprlem  7422  recexprlemloc  7483  gt0ap0  8432  ltap  8439  recexaplem2  8457  nn1m1nn  8782  nn1gt1  8798  ltpnf  9617  mnflt  9619  xrltso  9632  xrpnfdc  9675  xrmnfdc  9676  exfzdc  10068  apbtwnz  10098  expnnval  10347  exp0  10348  bc0k  10554  bcpasc  10564  xrmaxadd  11082  sumdc  11179  zsumdc  11205  fsum3  11208  fisumss  11213  isumss2  11214  fsumsplit  11228  zproddc  11400  fprodseq  11404  infssuzex  11698  ctiunctlemudc  12006  suplociccreex  12830  djurclALT  13200  bj-nn0suc0  13339  trilpolemres  13431  trirec0  13433  nconstwlpolem  13453
 Copyright terms: Public domain W3C validator