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  601  exdistrfor  1849  mopick2  2166  ssrexf  3304  ssrexv  3307  ssdif  3358  ssrin  3450  reupick  3509  disjss1  4096  copsexg  4365  po3nr  4436  coss2  4916  fununi  5429  fiintim  7204  recexprlemlol  7957  recexprlemupu  7959  icoshft  10345  2ffzeq  10500  qbtwnxr  10644  ico0  10648  r19.2uz  11707  bezoutlemzz  12727  bezoutlemaz  12728  ptex  13565  rnglidlmmgm  14774  neiss  15145  uptx  15269  txcn  15270  bj-charfundcALT  16719