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

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

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  586  exdistrfor  1772  mopick2  2082  ssrexf  3159  ssrexv  3162  ssdif  3211  ssrin  3301  reupick  3360  disjss1  3912  copsexg  4166  po3nr  4232  coss2  4695  fununi  5191  fiintim  6817  recexprlemlol  7434  recexprlemupu  7436  icoshft  9773  2ffzeq  9918  qbtwnxr  10035  ico0  10039  r19.2uz  10765  bezoutlemzz  11690  bezoutlemaz  11691  neiss  12319  uptx  12443  txcn  12444