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  2080  ssrexf  3154  ssrexv  3157  ssdif  3206  ssrin  3296  reupick  3355  disjss1  3907  copsexg  4161  po3nr  4227  coss2  4690  fununi  5186  fiintim  6810  recexprlemlol  7427  recexprlemupu  7429  icoshft  9766  2ffzeq  9911  qbtwnxr  10028  ico0  10032  r19.2uz  10758  bezoutlemzz  11679  bezoutlemaz  11680  neiss  12308  uptx  12432  txcn  12433