Theorem anim12i 331

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses

Ref	Expression
anim12i.1	⊢ (𝜑 → 𝜓)
anim12i.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
anim12i	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Proof of Theorem anim12i

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 ⊢ (𝜑 → 𝜓)
2		anim12i.2	. 2 ⊢ (𝜒 → 𝜃)
3		id 19	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 283	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  anim12ci  332  anim1i  333  anim2i  334  hban  1482  sbimi  1691  spsbbi  1769  2exeu  2037  cgsex2g  2649  cgsex4g  2650  spc2egv  2701  spc2gv  2702  sseq2  3037  unssin  3227  uneqin  3239  undif3ss  3249  prneimg  3603  ssunieq  3671  iuneq1  3728  iuneq2  3731  copsex2t  4048  soeq2  4119  tpexg  4245  eldifpw  4274  iunpw  4277  peano5  4388  opbrop  4487  xpsspw  4520  coeq1  4563  coeq2  4564  cnveq  4580  dmeq  4606  sotri  4796  elxp4  4886  elxp5  4887  funun  5025  funtp  5034  imain  5063  2elresin  5092  funssxp  5146  fssres  5152  f1co  5193  foun  5237  resdif  5240  f1oco  5241  fvun1  5335  fvreseq  5368  ftpg  5446  f1o2ndf1  5952  spc2ed  5957  smores  6013  nnaord  6222  nnm00  6242  brecop  6336  eroveu  6337  ecopovtrn  6343  ecopovtrng  6346  th3qlem1  6348  th3q  6351  addcmpblnq  6873  mulcmpblnq  6874  mulclnq  6882  dmaddpq  6885  dmmulpq  6886  mulcanenq  6891  distrnqg  6893  ltdcnq  6903  ltexnqq  6914  enq0breq  6942  mulcmpblnq0  6950  mulcanenq0ec  6951  addnnnq0  6955  mulnnnq0  6956  mulclnq0  6958  nqpnq0nq  6959  nqnq0a  6960  nqnq0m  6961  distrnq0  6965  elinp  6980  genpml  7023  genpmu  7024  genprndl  7027  genprndu  7028  addnqprl  7035  addnqpru  7036  distrlem1prl  7088  distrlem1pru  7089  ltsopr  7102  cauappcvgprlemdisj  7157  caucvgprlemdisj  7180  caucvgprprlemdisj  7208  addcmpblnr  7232  addsrpr  7238  mulsrpr  7239  addclsr  7246  addasssrg  7249  0idsr  7260  1idsr  7261  00sr  7262  mulgt0sr  7270  axaddcl  7348  axmulcl  7350  axaddass  7354  axdistr  7356  cnegexlem3  7606  cnegex  7607  apirr  8026  recexaplem2  8063  zletric  8730  zlelttric  8731  qaddcl  9055  qmulcl  9057  qreccl  9062  iccss  9294  fzsubel  9408  elfz0add  9465  difelfznle  9477  2ffzeq  9483  fzonmapblen  9529  ubmelfzo  9542  ubmelm1fzo  9568  subfzo0  9584  qletric  9586  qlelttric  9587  adddivflid  9630  mulexp  9896  mulexpzap  9897  leexp1a  9912  faclbnd  10049  rexanuz  10320  sqabsadd  10387  sqabssub  10388  abs2dif  10438  summodnegmod  10733  dvds2ln  10735  dvdsflip  10758  gcdsupex  10855  gcdsupcl  10856  gcdabs  10885  sqgcd  10924  lcmabs  10964  lcmgcdlem  10965  lcmgcd  10966  lcmgcdeq  10971  qredeq  10984  cncongr1  10991  cncongr2  10992  hashgcdlem  11109  bj-indind  11296