Theorem anim1i 323

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

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  sylanl1  382  sylanr1  384  mpan10  443  sbcof2  1691  sbidm  1731  disamis  2011  fun11uni  4969  fabexg  5077  fores  5115  f1oabexg  5138  fun11iun  5147  fvelrnb  5221  ssimaex  5234  foeqcnvco  5430  f1eqcocnv  5431  isoini  5457  brtposg  5869  elni2  6412  dmaddpqlem  6475  nqpi  6476  ltexnqq  6506  nq0nn  6540  nqnq0a  6552  nqnq0m  6553  elnp1st2nd  6574  mullocprlem  6668  cnegexlem3  7188  lediv2a  7861  btwnz  8357  eluz2b2  8540  uz2mulcl  8545  eqreznegel  8549  elioo4g  8803  fz0fzelfz0  8984  fz0fzdiffz0  8987  2ffzeq  8998  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  zpnn0elfzo  9063  expcl2lemap  9267  mulreap  9464  redivap  9474  imdivap  9481  caucvgrelemcau  9579