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

Theorem anim1d 329
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 328 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm3.45  564  exdistrfor  1728  mopick2  2031  ssrexv  3084  ssdif  3133  ssrin  3223  reupick  3281  disjss1  3820  copsexg  4062  po3nr  4128  coss2  4580  fununi  5068  recexprlemlol  7164  recexprlemupu  7166  icoshft  9376  2ffzeq  9517  qbtwnxr  9634  ico0  9638  r19.2uz  10391  bezoutlemzz  11084  bezoutlemaz  11085
  Copyright terms: Public domain W3C validator