Theorem anim2d 320

Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1d.1	⊢ (φ → (ψ → χ))

Assertion

Ref	Expression
anim2d	⊢ (φ → ((θ ∧ ψ) → (θ ∧ χ)))

Proof of Theorem anim2d

Step	Hyp	Ref	Expression
1		idd 21	. 2 ⊢ (φ → (θ → θ))
2		anim1d.1	. 2 ⊢ (φ → (ψ → χ))
3	1, 2	anim12d 318	1 ⊢ (φ → ((θ ∧ ψ) → (θ ∧ χ)))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  spsbim  1721  ssel  2933  sscon  3071  uniss  3592  trel3  3853  copsexg  3972  ssopab2  4003  coss1  4434  fununi  4910  imadif  4922  fss  4997  ssimaex  5177  opabbrex  5491  ssoprab2  5503  poxp  5794  xpdom2  6241