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

Theorem anim1d 334
 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 333 1 (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm3.45  587  exdistrfor  1773  mopick2  2083  ssrexf  3164  ssrexv  3167  ssdif  3216  ssrin  3306  reupick  3365  disjss1  3920  copsexg  4174  po3nr  4240  coss2  4703  fununi  5199  fiintim  6825  recexprlemlol  7459  recexprlemupu  7461  icoshft  9804  2ffzeq  9950  qbtwnxr  10067  ico0  10071  r19.2uz  10798  bezoutlemzz  11727  bezoutlemaz  11728  neiss  12359  uptx  12483  txcn  12484
 Copyright terms: Public domain W3C validator