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  anifpdc  992  hban  1593  sbimi  1810  spsbbi  1890  2exeu  2170  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  sseq2  3248  unssin  3443  uneqin  3455  undif3ss  3465  prneimg  3852  ssunieq  3921  iuneq1  3978  iuneq2  3981  copsex2t  4332  soeq2  4408  tpexg  4536  eldifpw  4569  iunpw  4572  peano5  4691  opbrop  4800  xpsspw  4833  coeq1  4882  coeq2  4883  cnveq  4899  dmeq  4926  sotri  5127  elxp4  5219  elxp5  5220  funun  5365  fununfun  5367  fundif  5368  funtp  5377  imain  5406  2elresin  5437  funssxp  5498  fssres  5506  f1co  5548  foun  5596  resdif  5599  f1oco  5600  fvun1  5705  elfvmptrab1  5734  fvreseq  5743  ftpg  5830  f1o2ndf1  6385  spc2ed  6390  smores  6449  nnaord  6668  nnm00  6689  brecop  6785  eroveu  6786  ecopovtrn  6792  ecopovtrng  6795  th3qlem1  6797  th3q  6800  ixpeq2  6872  djuexb  7227  addcmpblnq  7570  mulcmpblnq  7571  mulclnq  7579  dmaddpq  7582  dmmulpq  7583  mulcanenq  7588  distrnqg  7590  ltdcnq  7600  ltexnqq  7611  enq0breq  7639  mulcmpblnq0  7647  mulcanenq0ec  7648  addnnnq0  7652  mulnnnq0  7653  mulclnq0  7655  nqpnq0nq  7656  nqnq0a  7657  nqnq0m  7658  distrnq0  7662  elinp  7677  genpml  7720  genpmu  7721  genprndl  7724  genprndu  7725  addnqprl  7732  addnqpru  7733  distrlem1prl  7785  distrlem1pru  7786  ltsopr  7799  cauappcvgprlemdisj  7854  caucvgprlemdisj  7877  caucvgprprlemdisj  7905  addcmpblnr  7942  addsrpr  7948  mulsrpr  7949  addclsr  7956  addasssrg  7959  0idsr  7970  1idsr  7971  00sr  7972  mulgt0sr  7981  axaddcl  8067  axmulcl  8069  axaddass  8075  axdistr  8077  cnegexlem3  8339  cnegex  8340  apirr  8768  recexaplem2  8815  zletric  9506  zlelttric  9507  difgtsumgt  9532  qaddcl  9847  qmulcl  9849  qreccl  9854  iccss  10154  fzsubel  10273  elfz0add  10333  difelfznle  10348  2ffzeq  10354  fzonmapblen  10404  ubmelfzo  10423  ubmelm1fzo  10449  subfzo0  10465  qletric  10478  qlelttric  10479  adddivflid  10529  mulexp  10817  mulexpzap  10818  leexp1a  10833  faclbnd  10980  wrdeq  11111  ccatcl  11146  swrdsbslen  11219  swrdspsleq  11220  pfxccat1  11255  swrdswrdlem  11257  pfxccatin12lem2a  11280  swrdccatin2  11282  pfxccatin12lem2  11284  swrdccat  11288  reuccatpfxs1  11300  rexanuz  11520  sqabsadd  11587  sqabssub  11588  abs2dif  11638  rpmincl  11770  xrminrpcl  11806  fsum2dlemstep  11966  fprodeq0  12149  fprod2dlemstep  12154  summodnegmod  12354  dvds2ln  12356  dvdsflip  12383  gcdsupex  12499  gcdsupcl  12500  gcdabs  12530  sqgcd  12571  nnwosdc  12581  lcmabs  12619  lcmgcdlem  12620  lcmgcd  12621  lcmgcdeq  12626  qredeq  12639  cncongr1  12646  cncongr2  12647  hashgcdlem  12781  dvdsprmpweqle  12881  difsqpwdvds  12882  xpsfrnel2  13400  fngsum  13442  igsumvalx  13443  mndissubm  13529  resmhm2  13542  grpissubg  13752  subrngpropd  14201  subrgpropd  14238  tgcl  14759  uncld  14808  innei  14858  cnco  14916  txbas  14953  txbasval  14962  blin2  15127  qtopbasss  15216  lgsmulsqcoprm  15746  gausslemma2dlem1a  15758  lgsquad2lem2  15782  umgredgprv  15936  uspgredg2v  16040  usgredg2v  16043  wlkeq  16126  uspgr2wlkeq2  16138  uspgr2wlkeqi  16139  bj-charfunbi  16283  bj-indind  16404