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 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylanl2  407  sylanr2  409  andi  830  xoranor  1426  19.41h  1737  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbidm  1904  eu3h  2132  eupickb  2168  2exeu  2179  darii  2187  festino  2193  baroco  2194  r19.27v  2678  r19.27av  2686  rspc2ev  2945  reu3  3016  difdif  3354  ssddif  3465  inssdif  3467  difin  3468  difindiss  3485  indifdir  3487  difrab  3507  iundif2ss  4078  trssord  4527  ordsuc  4712  find  4748  imainss  5206  dffun5r  5392  fof  5618  f1ocnv  5655  fv3  5721  relelfvdm  5730  funimass4  5756  fvelimab  5762  funconstss  5830  dff2  5855  dffo5  5860  dff1o6  5985  oprabid  6120  ssoprab2i  6180  uchoice  6375  releldm2  6423  ixpf  7007  recexgt0sr  8147  map2psrprg  8179  lediv2a  9234  lbreu  9284  elfzp12  10524  fihashf1rn  11250  ccatsymb  11393  swrdpfx  11502  pfxpfx  11503  pfxccatin12  11528  cau3lem  11904  fsumcl2lem  12191  dvdsnegb  12601  dvds2add  12618  dvds2sub  12619  ndvdssub  12723  gcd2n0cl  12772  divgcdcoprmex  12906  cncongr1  12907  ballotfilemirc  13334  ctinfom  13378  qusecsub  14226  istopfin  15238  toponcom  15265  cnptoprest  15477  dvmptfsum  15963  elply2  15973  bpos1lem  16321  subupgr  16731  uspgr2wlkeqi  16825  clwwlknun  16899  alseuals  17384  ralseurals  17385