Theorem anim2i 342

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 338	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 is referenced by:  sylanl2  403  sylanr2  405  andi  818  pm4.55dc  938  xoranor  1377  19.41h  1685  sbimi  1764  equs5e  1795  exdistrfor  1800  equs45f  1802  sbidm  1851  eu3h  2071  eupickb  2107  2exeu  2118  darii  2126  festino  2132  baroco  2133  r19.27v  2604  r19.27av  2612  rspc2ev  2856  reu3  2927  difdif  3260  ssddif  3369  inssdif  3371  difin  3372  difindiss  3389  indifdir  3391  difrab  3409  iundif2ss  3952  trssord  4380  ordsuc  4562  find  4598  imainss  5044  dffun5r  5228  fof  5438  f1ocnv  5474  fv3  5538  relelfvdm  5547  funimass4  5566  fvelimab  5572  funconstss  5634  dff2  5660  dffo5  5665  dff1o6  5776  oprabid  5906  ssoprab2i  5963  releldm2  6185  ixpf  6719  recexgt0sr  7771  map2psrprg  7803  lediv2a  8851  lbreu  8901  elfzp12  10098  fihashf1rn  10767  cau3lem  11122  fsumcl2lem  11405  dvdsnegb  11814  dvds2add  11831  dvds2sub  11832  ndvdssub  11934  gcd2n0cl  11969  divgcdcoprmex  12101  cncongr1  12102  ctinfom  12428  istopfin  13470  toponcom  13497  cnptoprest  13709