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  995  hban  1596  sbimi  1813  spsbbi  1893  2exeu  2173  cgsex2g  2849  cgsex4g  2850  spc2egv  2906  spc2gv  2907  sseq2  3261  unssin  3459  uneqin  3471  undif3ss  3481  prneimg  3877  ssunieq  3946  iuneq1  4003  iuneq2  4006  copsex2t  4360  soeq2  4436  tpexg  4564  eldifpw  4597  iunpw  4600  peano5  4719  opbrop  4828  xpsspw  4861  coeq1  4911  coeq2  4912  cnveq  4928  dmeq  4955  sotri  5157  elxp4  5249  elxp5  5250  funun  5396  fununfun  5398  fundif  5399  funtp  5408  imain  5437  2elresin  5468  funssxp  5531  fssres  5539  f1co  5584  foun  5632  resdif  5635  f1oco  5636  fvun1  5742  elfvmptrab1  5771  fvreseq  5780  ftpg  5867  f1o2ndf1  6423  spc2ed  6428  fvn0elsupp  6450  smores  6522  nnaord  6741  nnm00  6762  brecop  6858  eroveu  6859  ecopovtrn  6865  ecopovtrng  6868  th3qlem1  6870  th3q  6873  ixpeq2  6946  djuexb  7334  addcmpblnq  7681  mulcmpblnq  7682  mulclnq  7690  dmaddpq  7693  dmmulpq  7694  mulcanenq  7699  distrnqg  7701  ltdcnq  7711  ltexnqq  7722  enq0breq  7750  mulcmpblnq0  7758  mulcanenq0ec  7759  addnnnq0  7763  mulnnnq0  7764  mulclnq0  7766  nqpnq0nq  7767  nqnq0a  7768  nqnq0m  7769  distrnq0  7773  elinp  7788  genpml  7831  genpmu  7832  genprndl  7835  genprndu  7836  addnqprl  7843  addnqpru  7844  distrlem1prl  7896  distrlem1pru  7897  ltsopr  7910  cauappcvgprlemdisj  7965  caucvgprlemdisj  7988  caucvgprprlemdisj  8016  addcmpblnr  8053  addsrpr  8059  mulsrpr  8060  addclsr  8067  addasssrg  8070  0idsr  8081  1idsr  8082  00sr  8083  mulgt0sr  8092  axaddcl  8178  axmulcl  8180  axaddass  8186  axdistr  8188  cnegexlem3  8449  cnegex  8450  apirr  8878  recexaplem2  8925  zletric  9620  zlelttric  9621  difgtsumgt  9646  qaddcl  9966  qmulcl  9968  qreccl  9973  iccss  10273  fzsubel  10393  elfz0add  10453  difelfznle  10468  2ffzeq  10474  fzonmapblen  10525  ubmelfzo  10544  ubmelm1fzo  10570  subfzo0  10587  qletric  10600  qlelttric  10601  adddivflid  10651  mulexp  10939  mulexpzap  10940  leexp1a  10955  faclbnd  11102  wrdeq  11242  ccatcl  11277  swrdsbslen  11354  swrdspsleq  11355  pfxccat1  11390  swrdswrdlem  11392  pfxccatin12lem2a  11415  swrdccatin2  11417  pfxccatin12lem2  11419  swrdccat  11423  reuccatpfxs1  11435  rexanuz  11669  sqabsadd  11736  sqabssub  11737  abs2dif  11787  rpmincl  11919  xrminrpcl  11955  fsum2dlemstep  12116  fprodeq0  12299  fprod2dlemstep  12304  summodnegmod  12504  dvds2ln  12506  dvdsflip  12533  gcdsupex  12649  gcdsupcl  12650  gcdabs  12680  sqgcd  12721  nnwosdc  12731  lcmabs  12769  lcmgcdlem  12770  lcmgcd  12771  lcmgcdeq  12776  qredeq  12789  cncongr1  12796  cncongr2  12797  hashgcdlem  12931  dvdsprmpweqle  13031  difsqpwdvds  13032  xpsfrnel2  13551  fngsum  13593  igsumvalx  13594  mndissubm  13680  resmhm2  13693  grpissubg  13903  subrngpropd  14353  subrgpropd  14390  tgcl  14921  uncld  14970  innei  15020  cnco  15078  txbas  15115  txbasval  15124  blin2  15289  qtopbasss  15378  lgsmulsqcoprm  15911  gausslemma2dlem1a  15923  lgsquad2lem2  15947  umgredgprv  16102  uspgredg2v  16208  usgredg2v  16211  wlkeq  16341  uspgr2wlkeq2  16353  uspgr2wlkeqi  16354  clwwlknonex2  16426  bj-charfunbi  16573  bj-indind  16694