Theorem anim1d 336

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

Step	Hyp	Ref	Expression
1		anim1d.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 21	. 2 ⊢ (𝜑 → (𝜃 → 𝜃))
3	1, 2	anim12d 335	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm3.45  597  exdistrfor  1824  mopick2  2138  ssrexf  3256  ssrexv  3259  ssdif  3309  ssrin  3399  reupick  3458  disjss1  4029  copsexg  4292  po3nr  4361  coss2  4838  fununi  5347  fiintim  7035  recexprlemlol  7746  recexprlemupu  7748  icoshft  10119  2ffzeq  10270  qbtwnxr  10407  ico0  10411  r19.2uz  11348  bezoutlemzz  12367  bezoutlemaz  12368  ptex  13140  rnglidlmmgm  14302  neiss  14666  uptx  14790  txcn  14791  bj-charfundcALT  15819