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  823  xoranor  1419  19.41h  1731  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbidm  1897  eu3h  2123  eupickb  2159  2exeu  2170  darii  2178  festino  2184  baroco  2185  r19.27v  2658  r19.27av  2666  rspc2ev  2922  reu3  2993  difdif  3329  ssddif  3438  inssdif  3440  difin  3441  difindiss  3458  indifdir  3460  difrab  3478  iundif2ss  4031  trssord  4471  ordsuc  4655  find  4691  imainss  5144  dffun5r  5330  fof  5550  f1ocnv  5587  fv3  5652  relelfvdm  5661  funimass4  5686  fvelimab  5692  funconstss  5755  dff2  5781  dffo5  5786  dff1o6  5906  oprabid  6039  ssoprab2i  6099  uchoice  6289  releldm2  6337  ixpf  6875  recexgt0sr  7968  map2psrprg  8000  lediv2a  9050  lbreu  9100  elfzp12  10303  fihashf1rn  11018  ccatsymb  11145  swrdpfx  11247  pfxpfx  11248  pfxccatin12  11273  cau3lem  11633  fsumcl2lem  11917  dvdsnegb  12327  dvds2add  12344  dvds2sub  12345  ndvdssub  12449  gcd2n0cl  12498  divgcdcoprmex  12632  cncongr1  12633  ctinfom  13007  qusecsub  13876  istopfin  14682  toponcom  14709  cnptoprest  14921  dvmptfsum  15407  elply2  15417  uspgr2wlkeqi  16088