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

Theorem anim1d 319
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
anim1d.1 (φ → (ψχ))
Assertion
Ref Expression
anim1d (φ → ((ψ θ) → (χ θ)))

Proof of Theorem anim1d
StepHypRef Expression
1 anim1d.1 . 2 (φ → (ψχ))
2 idd 21 . 2 (φ → (θθ))
31, 2anim12d 318 1 (φ → ((ψ θ) → (χ θ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm3.45  529  exdistrfor  1678  mopick2  1980  ssrexv  2999  ssdif  3072  ssrin  3156  reupick  3215  disjss1  3742  copsexg  3972  po3nr  4038  coss2  4435  fununi  4910  recexprlemlol  6597  recexprlemupu  6599  icoshft  8608  2ffzeq  8748
  Copyright terms: Public domain W3C validator