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  825  xoranor  1421  19.41h  1733  sbimi  1812  equs5e  1843  exdistrfor  1848  equs45f  1850  sbidm  1899  eu3h  2125  eupickb  2161  2exeu  2172  darii  2180  festino  2186  baroco  2187  r19.27v  2660  r19.27av  2668  rspc2ev  2925  reu3  2996  difdif  3332  ssddif  3441  inssdif  3443  difin  3444  difindiss  3461  indifdir  3463  difrab  3481  iundif2ss  4036  trssord  4477  ordsuc  4661  find  4697  imainss  5152  dffun5r  5338  fof  5559  f1ocnv  5596  fv3  5662  relelfvdm  5671  funimass4  5696  fvelimab  5702  funconstss  5765  dff2  5791  dffo5  5796  dff1o6  5917  oprabid  6050  ssoprab2i  6110  uchoice  6300  releldm2  6348  ixpf  6889  recexgt0sr  7993  map2psrprg  8025  lediv2a  9075  lbreu  9125  elfzp12  10334  fihashf1rn  11051  ccatsymb  11180  swrdpfx  11289  pfxpfx  11290  pfxccatin12  11315  cau3lem  11676  fsumcl2lem  11961  dvdsnegb  12371  dvds2add  12388  dvds2sub  12389  ndvdssub  12493  gcd2n0cl  12542  divgcdcoprmex  12676  cncongr1  12677  ctinfom  13051  qusecsub  13920  istopfin  14727  toponcom  14754  cnptoprest  14966  dvmptfsum  15452  elply2  15462  subupgr  16127  uspgr2wlkeqi  16221  clwwlknun  16295