Theorem anim12i 338

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  anim12ci  339  anim1i  340  anim2i  342  hban  1558  sbimi  1775  spsbbi  1855  2exeu  2134  cgsex2g  2796  cgsex4g  2797  spc2egv  2850  spc2gv  2851  sseq2  3203  unssin  3398  uneqin  3410  undif3ss  3420  prneimg  3800  ssunieq  3868  iuneq1  3925  iuneq2  3928  copsex2t  4274  soeq2  4347  tpexg  4475  eldifpw  4508  iunpw  4511  peano5  4630  opbrop  4738  xpsspw  4771  coeq1  4819  coeq2  4820  cnveq  4836  dmeq  4862  sotri  5061  elxp4  5153  elxp5  5154  funun  5298  funtp  5307  imain  5336  2elresin  5365  funssxp  5423  fssres  5429  f1co  5471  foun  5519  resdif  5522  f1oco  5523  fvun1  5623  elfvmptrab1  5652  fvreseq  5661  ftpg  5742  f1o2ndf1  6281  spc2ed  6286  smores  6345  nnaord  6562  nnm00  6583  brecop  6679  eroveu  6680  ecopovtrn  6686  ecopovtrng  6689  th3qlem1  6691  th3q  6694  ixpeq2  6766  djuexb  7103  addcmpblnq  7427  mulcmpblnq  7428  mulclnq  7436  dmaddpq  7439  dmmulpq  7440  mulcanenq  7445  distrnqg  7447  ltdcnq  7457  ltexnqq  7468  enq0breq  7496  mulcmpblnq0  7504  mulcanenq0ec  7505  addnnnq0  7509  mulnnnq0  7510  mulclnq0  7512  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  distrnq0  7519  elinp  7534  genpml  7577  genpmu  7578  genprndl  7581  genprndu  7582  addnqprl  7589  addnqpru  7590  distrlem1prl  7642  distrlem1pru  7643  ltsopr  7656  cauappcvgprlemdisj  7711  caucvgprlemdisj  7734  caucvgprprlemdisj  7762  addcmpblnr  7799  addsrpr  7805  mulsrpr  7806  addclsr  7813  addasssrg  7816  0idsr  7827  1idsr  7828  00sr  7829  mulgt0sr  7838  axaddcl  7924  axmulcl  7926  axaddass  7932  axdistr  7934  cnegexlem3  8196  cnegex  8197  apirr  8624  recexaplem2  8671  zletric  9361  zlelttric  9362  difgtsumgt  9386  qaddcl  9700  qmulcl  9702  qreccl  9707  iccss  10007  fzsubel  10126  elfz0add  10186  difelfznle  10201  2ffzeq  10207  fzonmapblen  10254  ubmelfzo  10267  ubmelm1fzo  10293  subfzo0  10309  qletric  10311  qlelttric  10312  adddivflid  10361  mulexp  10649  mulexpzap  10650  leexp1a  10665  faclbnd  10812  wrdeq  10936  rexanuz  11132  sqabsadd  11199  sqabssub  11200  abs2dif  11250  rpmincl  11381  xrminrpcl  11417  fsum2dlemstep  11577  fprodeq0  11760  fprod2dlemstep  11765  summodnegmod  11965  dvds2ln  11967  dvdsflip  11993  gcdsupex  12094  gcdsupcl  12095  gcdabs  12125  sqgcd  12166  nnwosdc  12176  lcmabs  12214  lcmgcdlem  12215  lcmgcd  12216  lcmgcdeq  12221  qredeq  12234  cncongr1  12241  cncongr2  12242  hashgcdlem  12376  dvdsprmpweqle  12475  difsqpwdvds  12476  xpsfrnel2  12929  fngsum  12971  igsumvalx  12972  mndissubm  13047  resmhm2  13060  grpissubg  13264  subrngpropd  13712  subrgpropd  13749  tgcl  14232  uncld  14281  innei  14331  cnco  14389  txbas  14426  txbasval  14435  blin2  14600  qtopbasss  14689  lgsmulsqcoprm  15162  gausslemma2dlem1a  15174  bj-charfunbi  15303  bj-indind  15424