Theorem anim1i 340

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 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:  sylanl1  406  sylanr1  408  mpan10  478  sbcof2  1863  sbidm  1904  disamis  2198  r19.28v  2679  fun11uni  5454  fabexg  5582  fores  5628  f1oabexg  5654  fun11iun  5663  fdmeu  5749  fvelrnb  5753  ssimaex  5767  foeqcnvco  5999  f1eqcocnv  6000  isoini  6027  brtposg  6529  tfrcllemssrecs  6627  fiintim  7243  djuex  7390  elni2  7688  dmaddpqlem  7751  nqpi  7752  ltexnqq  7782  nq0nn  7816  nqnq0a  7828  nqnq0m  7829  elnp1st2nd  7850  mullocprlem  7944  cnegexlem3  8511  divmulasscomap  9035  lediv2a  9234  btwnz  9777  eluz2b2  10020  uz2mulcl  10025  eqreznegel  10031  elioo4g  10354  fz0fzelfz0  10552  fz0fzdiffz0  10555  2ffzeq  10566  elfzodifsumelfzo  10637  elfzom1elp1fzo  10638  zpnn0elfzo  10643  infssuzex  10684  ioo0  10712  zmodidfzoimp  10813  expcl2lemap  11010  hashfibclem  11305  iswrdsymb  11345  ccatcl  11384  ccatsymb  11393  swrdfv2  11458  swrdsbslen  11461  swrdspsleq  11462  pfxswrd  11501  pfxccatin12lem3  11527  pfxccatpfx2  11532  swrdccat3blem  11534  reuccatpfxs1  11542  mulreap  11652  redivap  11662  imdivap  11669  caucvgrelemcau  11769  zproddc  12372  fprodseq  12376  p1modz1  12587  negdvdsb  12600  muldvds1  12609  muldvds2  12610  dvdsdivcl  12643  nn0ehalf  12696  nn0oddm1d2  12702  nnoddm1d2  12703  divgcdnn  12778  coprmgcdb  12892  divgcdcoprm0  12905  pwbdvdslemn  12970  oddprmdvds  13163  4sqexercise1  13207  4sqexercise2  13208  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemth  13340  grpissubg  14057  ecqusaddd  14101  ecqusaddcl  14102  rnglz  14352  qusmulrng  14979  quscrng  14980  dvdsrzring  15048  bcmono  16316  lgsprme0  16378  gausslemma2dlem0e  16389  gausslemma2dlem1a  16394  gausslemma2dlem6  16403  lgsquadlem2  16414  2lgsoddprm  16449  usgrislfuspgrdom  16648  edgssv2en  16657  umgr2edg  16665  uspgredg2v  16679  subupgr  16731  subusgr  16733  vtxdfifiun  16755  eupth2lem3lem3fi  16928