Theorem anim1i 336

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylanl1  397  sylanr1  399  mpan10  463  sbcof2  1764  sbidm  1805  disamis  2086  r19.28v  2534  fun11uni  5151  fabexg  5268  fores  5312  f1oabexg  5335  fun11iun  5344  fvelrnb  5423  ssimaex  5436  foeqcnvco  5645  f1eqcocnv  5646  isoini  5673  brtposg  6105  tfrcllemssrecs  6203  fiintim  6770  djuex  6880  elni2  7070  dmaddpqlem  7133  nqpi  7134  ltexnqq  7164  nq0nn  7198  nqnq0a  7210  nqnq0m  7211  elnp1st2nd  7232  mullocprlem  7326  cnegexlem3  7862  divmulasscomap  8369  lediv2a  8563  btwnz  9074  eluz2b2  9299  uz2mulcl  9304  eqreznegel  9308  elioo4g  9610  fz0fzelfz0  9797  fz0fzdiffz0  9800  2ffzeq  9811  elfzodifsumelfzo  9871  elfzom1elp1fzo  9872  zpnn0elfzo  9877  ioo0  9930  zmodidfzoimp  10020  expcl2lemap  10198  mulreap  10529  redivap  10539  imdivap  10546  caucvgrelemcau  10644  negdvdsb  11357  muldvds1  11366  muldvds2  11367  dvdsdivcl  11396  nn0ehalf  11448  nn0oddm1d2  11454  nnoddm1d2  11455  infssuzex  11490  divgcdnn  11511  coprmgcdb  11615  divgcdcoprm0  11628  pw2dvdslemn  11688