Theorem anim1i 338

Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
anim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
anim1i	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Proof of Theorem anim1i

Step	Hyp	Ref	Expression
1		anim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 19	. 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:  sylanl1  400  sylanr1  402  mpan10  466  sbcof2  1790  sbidm  1831  disamis  2117  r19.28v  2585  fun11uni  5237  fabexg  5354  fores  5398  f1oabexg  5423  fun11iun  5432  fvelrnb  5513  ssimaex  5526  foeqcnvco  5735  f1eqcocnv  5736  isoini  5763  brtposg  6195  tfrcllemssrecs  6293  fiintim  6866  djuex  6977  elni2  7217  dmaddpqlem  7280  nqpi  7281  ltexnqq  7311  nq0nn  7345  nqnq0a  7357  nqnq0m  7358  elnp1st2nd  7379  mullocprlem  7473  cnegexlem3  8035  divmulasscomap  8552  lediv2a  8749  btwnz  9266  eluz2b2  9496  uz2mulcl  9501  eqreznegel  9505  elioo4g  9820  fz0fzelfz0  10008  fz0fzdiffz0  10011  2ffzeq  10022  elfzodifsumelfzo  10082  elfzom1elp1fzo  10083  zpnn0elfzo  10088  ioo0  10141  zmodidfzoimp  10235  expcl2lemap  10413  mulreap  10746  redivap  10756  imdivap  10763  caucvgrelemcau  10862  zproddc  11458  fprodseq  11462  p1modz1  11672  negdvdsb  11684  muldvds1  11693  muldvds2  11694  dvdsdivcl  11723  nn0ehalf  11775  nn0oddm1d2  11781  nnoddm1d2  11782  infssuzex  11817  divgcdnn  11839  coprmgcdb  11945  divgcdcoprm0  11958  pw2dvdslemn  12019