Theorem anim2i 340

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

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  sylanl2  401  sylanr2  403  andi  808  pm4.55dc  927  xoranor  1366  19.41h  1672  sbimi  1751  equs5e  1782  exdistrfor  1787  equs45f  1789  sbidm  1838  eu3h  2058  eupickb  2094  2exeu  2105  darii  2113  festino  2119  baroco  2120  r19.27v  2591  r19.27av  2599  rspc2ev  2840  reu3  2911  difdif  3242  ssddif  3351  inssdif  3353  difin  3354  difindiss  3371  indifdir  3373  difrab  3391  iundif2ss  3925  trssord  4352  ordsuc  4534  find  4570  imainss  5013  dffun5r  5194  fof  5404  f1ocnv  5439  fv3  5503  relelfvdm  5512  funimass4  5531  fvelimab  5536  funconstss  5597  dff2  5623  dffo5  5628  dff1o6  5738  oprabid  5865  ssoprab2i  5922  releldm2  6145  ixpf  6677  recexgt0sr  7705  map2psrprg  7737  lediv2a  8781  lbreu  8831  elfzp12  10024  focdmex  10689  fihashf1rn  10691  cau3lem  11042  fsumcl2lem  11325  dvdsnegb  11734  dvds2add  11751  dvds2sub  11752  ndvdssub  11852  gcd2n0cl  11887  divgcdcoprmex  12013  cncongr1  12014  ctinfom  12298  istopfin  12539  toponcom  12566  cnptoprest  12780