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  2857  reu3  2928  difdif  3261  ssddif  3370  inssdif  3372  difin  3373  difindiss  3390  indifdir  3392  difrab  3410  iundif2ss  3953  trssord  4381  ordsuc  4563  find  4599  imainss  5045  dffun5r  5229  fof  5439  f1ocnv  5475  fv3  5539  relelfvdm  5548  funimass4  5567  fvelimab  5573  funconstss  5635  dff2  5661  dffo5  5666  dff1o6  5777  oprabid  5907  ssoprab2i  5964  releldm2  6186  ixpf  6720  recexgt0sr  7772  map2psrprg  7804  lediv2a  8852  lbreu  8902  elfzp12  10099  fihashf1rn  10768  cau3lem  11123  fsumcl2lem  11406  dvdsnegb  11815  dvds2add  11832  dvds2sub  11833  ndvdssub  11935  gcd2n0cl  11970  divgcdcoprmex  12102  cncongr1  12103  ctinfom  12429  istopfin  13503  toponcom  13530  cnptoprest  13742