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  994  hban  1595  sbimi  1812  spsbbi  1892  2exeu  2172  cgsex2g  2839  cgsex4g  2840  spc2egv  2896  spc2gv  2897  sseq2  3251  unssin  3446  uneqin  3458  undif3ss  3468  prneimg  3857  ssunieq  3926  iuneq1  3983  iuneq2  3986  copsex2t  4337  soeq2  4413  tpexg  4541  eldifpw  4574  iunpw  4577  peano5  4696  opbrop  4805  xpsspw  4838  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  sotri  5132  elxp4  5224  elxp5  5225  funun  5371  fununfun  5373  fundif  5374  funtp  5383  imain  5412  2elresin  5443  funssxp  5504  fssres  5512  f1co  5554  foun  5602  resdif  5605  f1oco  5606  fvun1  5712  elfvmptrab1  5741  fvreseq  5750  ftpg  5838  f1o2ndf1  6393  spc2ed  6398  smores  6458  nnaord  6677  nnm00  6698  brecop  6794  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem1  6806  th3q  6809  ixpeq2  6881  djuexb  7243  addcmpblnq  7587  mulcmpblnq  7588  mulclnq  7596  dmaddpq  7599  dmmulpq  7600  mulcanenq  7605  distrnqg  7607  ltdcnq  7617  ltexnqq  7628  enq0breq  7656  mulcmpblnq0  7664  mulcanenq0ec  7665  addnnnq0  7669  mulnnnq0  7670  mulclnq0  7672  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  elinp  7694  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  addnqprl  7749  addnqpru  7750  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  cauappcvgprlemdisj  7871  caucvgprlemdisj  7894  caucvgprprlemdisj  7922  addcmpblnr  7959  addsrpr  7965  mulsrpr  7966  addclsr  7973  addasssrg  7976  0idsr  7987  1idsr  7988  00sr  7989  mulgt0sr  7998  axaddcl  8084  axmulcl  8086  axaddass  8092  axdistr  8094  cnegexlem3  8356  cnegex  8357  apirr  8785  recexaplem2  8832  zletric  9523  zlelttric  9524  difgtsumgt  9549  qaddcl  9869  qmulcl  9871  qreccl  9876  iccss  10176  fzsubel  10295  elfz0add  10355  difelfznle  10370  2ffzeq  10376  fzonmapblen  10427  ubmelfzo  10446  ubmelm1fzo  10472  subfzo0  10489  qletric  10502  qlelttric  10503  adddivflid  10553  mulexp  10841  mulexpzap  10842  leexp1a  10857  faclbnd  11004  wrdeq  11139  ccatcl  11174  swrdsbslen  11251  swrdspsleq  11252  pfxccat1  11287  swrdswrdlem  11289  pfxccatin12lem2a  11312  swrdccatin2  11314  pfxccatin12lem2  11316  swrdccat  11320  reuccatpfxs1  11332  rexanuz  11553  sqabsadd  11620  sqabssub  11621  abs2dif  11671  rpmincl  11803  xrminrpcl  11839  fsum2dlemstep  12000  fprodeq0  12183  fprod2dlemstep  12188  summodnegmod  12388  dvds2ln  12390  dvdsflip  12417  gcdsupex  12533  gcdsupcl  12534  gcdabs  12564  sqgcd  12605  nnwosdc  12615  lcmabs  12653  lcmgcdlem  12654  lcmgcd  12655  lcmgcdeq  12660  qredeq  12673  cncongr1  12680  cncongr2  12681  hashgcdlem  12815  dvdsprmpweqle  12915  difsqpwdvds  12916  xpsfrnel2  13434  fngsum  13476  igsumvalx  13477  mndissubm  13563  resmhm2  13576  grpissubg  13786  subrngpropd  14236  subrgpropd  14273  tgcl  14794  uncld  14843  innei  14893  cnco  14951  txbas  14988  txbasval  14997  blin2  15162  qtopbasss  15251  lgsmulsqcoprm  15781  gausslemma2dlem1a  15793  lgsquad2lem2  15817  umgredgprv  15972  uspgredg2v  16078  usgredg2v  16081  wlkeq  16211  uspgr2wlkeq2  16223  uspgr2wlkeqi  16224  clwwlknonex2  16296  bj-charfunbi  16432  bj-indind  16553