Theorem anim2i 337

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim2i	⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

Proof of Theorem anim2i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜒 → 𝜒)
2		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 334	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 is referenced by:  sylanl2  398  sylanr2  400  andi  773  pm4.55dc  890  xoranor  1323  19.41h  1631  sbimi  1705  equs5e  1734  exdistrfor  1739  equs45f  1741  sbidm  1790  eu3h  2005  eupickb  2041  2exeu  2052  darii  2060  festino  2066  baroco  2067  r19.27v  2518  r19.27av  2526  rspc2ev  2758  reu3  2827  difdif  3148  ssddif  3257  inssdif  3259  difin  3260  difindiss  3277  indifdir  3279  difrab  3297  iundif2ss  3825  trssord  4240  ordsuc  4416  find  4451  imainss  4890  dffun5r  5071  fof  5281  f1ocnv  5314  fv3  5376  relelfvdm  5385  funimass4  5404  fvelimab  5409  funconstss  5470  dff2  5496  dffo5  5501  dff1o6  5609  oprabid  5735  ssoprab2i  5792  releldm2  6013  ixpf  6544  recexgt0sr  7469  lediv2a  8511  lbreu  8561  elfzp12  9720  focdmex  10374  fihashf1rn  10376  cau3lem  10726  fsumcl2lem  11006  dvdsnegb  11305  dvds2add  11322  dvds2sub  11323  ndvdssub  11422  gcd2n0cl  11453  divgcdcoprmex  11576  cncongr1  11577  ctinfom  11733  istopfin  11949  toponcom  11976  cnptoprest  12189