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  4331  soeq2  4407  tpexg  4535  eldifpw  4568  iunpw  4571  peano5  4690  opbrop  4798  xpsspw  4831  coeq1  4879  coeq2  4880  cnveq  4896  dmeq  4923  sotri  5124  elxp4  5216  elxp5  5217  funun  5362  fununfun  5364  fundif  5365  funtp  5374  imain  5403  2elresin  5434  funssxp  5495  fssres  5503  f1co  5545  foun  5593  resdif  5596  f1oco  5597  fvun1  5702  elfvmptrab1  5731  fvreseq  5740  ftpg  5827  f1o2ndf1  6380  spc2ed  6385  smores  6444  nnaord  6663  nnm00  6684  brecop  6780  eroveu  6781  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  th3q  6795  ixpeq2  6867  djuexb  7219  addcmpblnq  7562  mulcmpblnq  7563  mulclnq  7571  dmaddpq  7574  dmmulpq  7575  mulcanenq  7580  distrnqg  7582  ltdcnq  7592  ltexnqq  7603  enq0breq  7631  mulcmpblnq0  7639  mulcanenq0ec  7640  addnnnq0  7644  mulnnnq0  7645  mulclnq0  7647  nqpnq0nq  7648  nqnq0a  7649  nqnq0m  7650  distrnq0  7654  elinp  7669  genpml  7712  genpmu  7713  genprndl  7716  genprndu  7717  addnqprl  7724  addnqpru  7725  distrlem1prl  7777  distrlem1pru  7778  ltsopr  7791  cauappcvgprlemdisj  7846  caucvgprlemdisj  7869  caucvgprprlemdisj  7897  addcmpblnr  7934  addsrpr  7940  mulsrpr  7941  addclsr  7948  addasssrg  7951  0idsr  7962  1idsr  7963  00sr  7964  mulgt0sr  7973  axaddcl  8059  axmulcl  8061  axaddass  8067  axdistr  8069  cnegexlem3  8331  cnegex  8332  apirr  8760  recexaplem2  8807  zletric  9498  zlelttric  9499  difgtsumgt  9524  qaddcl  9838  qmulcl  9840  qreccl  9845  iccss  10145  fzsubel  10264  elfz0add  10324  difelfznle  10339  2ffzeq  10345  fzonmapblen  10395  ubmelfzo  10414  ubmelm1fzo  10440  subfzo0  10456  qletric  10469  qlelttric  10470  adddivflid  10520  mulexp  10808  mulexpzap  10809  leexp1a  10824  faclbnd  10971  wrdeq  11101  ccatcl  11136  swrdsbslen  11206  swrdspsleq  11207  pfxccat1  11242  swrdswrdlem  11244  pfxccatin12lem2a  11267  swrdccatin2  11269  pfxccatin12lem2  11271  swrdccat  11275  reuccatpfxs1  11287  rexanuz  11507  sqabsadd  11574  sqabssub  11575  abs2dif  11625  rpmincl  11757  xrminrpcl  11793  fsum2dlemstep  11953  fprodeq0  12136  fprod2dlemstep  12141  summodnegmod  12341  dvds2ln  12343  dvdsflip  12370  gcdsupex  12486  gcdsupcl  12487  gcdabs  12517  sqgcd  12558  nnwosdc  12568  lcmabs  12606  lcmgcdlem  12607  lcmgcd  12608  lcmgcdeq  12613  qredeq  12626  cncongr1  12633  cncongr2  12634  hashgcdlem  12768  dvdsprmpweqle  12868  difsqpwdvds  12869  xpsfrnel2  13387  fngsum  13429  igsumvalx  13430  mndissubm  13516  resmhm2  13529  grpissubg  13739  subrngpropd  14188  subrgpropd  14225  tgcl  14746  uncld  14795  innei  14845  cnco  14903  txbas  14940  txbasval  14949  blin2  15114  qtopbasss  15203  lgsmulsqcoprm  15733  gausslemma2dlem1a  15745  lgsquad2lem2  15769  umgredgprv  15923  uspgredg2v  16027  usgredg2v  16030  wlkeq  16075  uspgr2wlkeq2  16087  uspgr2wlkeqi  16088  bj-charfunbi  16198  bj-indind  16319