Theorem anim1d 332

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 331	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  567  exdistrfor  1739  mopick2  2043  ssrexv  3109  ssdif  3158  ssrin  3248  reupick  3307  disjss1  3858  copsexg  4104  po3nr  4170  coss2  4633  fununi  5127  fiintim  6746  recexprlemlol  7335  recexprlemupu  7337  icoshft  9614  2ffzeq  9759  qbtwnxr  9876  ico0  9880  r19.2uz  10605  bezoutlemzz  11483  bezoutlemaz  11484  neiss  12101  uptx  12224  txcn  12225