Theorem anim2d 433

Description: Add a conjunct to left of antecedent and consequent in a deduction.

Hypothesis

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

Assertion

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

Proof of Theorem anim2d

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

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  anbi2d 468  eqvin.l1 851  moeq3 1432  ssel 1502  sscon 1599  uniss 1936  trel3 2049  ssopab2 2119  dfwe2 2187  relss 2480  fununi 2705  imadif 2714  tfrlem1 2949  xpdom2 3345  infsdomnn 3426  unfi2 3442  inf3lem1 3464  zfregs 3491  cfub 3703  cflim 3704  ltbtwnpq 3878  distrlem2pr 3922  ltexprlem3 3938  suppsr2 4017  axsup 4088  nnunb 4520  indstr 4611  infxpidmlem7 4939  shsubclt 5125  shintcl 5294  shmods 5363  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org