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  8850  lbreu  8900  elfzp12  10096  fihashf1rn  10763  cau3lem  11118  fsumcl2lem  11401  dvdsnegb  11810  dvds2add  11827  dvds2sub  11828  ndvdssub  11929  gcd2n0cl  11964  divgcdcoprmex  12096  cncongr1  12097  ctinfom  12423  istopfin  13391  toponcom  13418  cnptoprest  13632