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  1571  sbimi  1788  spsbbi  1868  2exeu  2147  cgsex2g  2810  cgsex4g  2811  spc2egv  2865  spc2gv  2866  sseq2  3219  unssin  3414  uneqin  3426  undif3ss  3436  prneimg  3818  ssunieq  3886  iuneq1  3943  iuneq2  3946  copsex2t  4294  soeq2  4368  tpexg  4496  eldifpw  4529  iunpw  4532  peano5  4651  opbrop  4759  xpsspw  4792  coeq1  4840  coeq2  4841  cnveq  4857  dmeq  4884  sotri  5084  elxp4  5176  elxp5  5177  funun  5321  fununfun  5323  fundif  5324  funtp  5333  imain  5362  2elresin  5393  funssxp  5452  fssres  5460  f1co  5502  foun  5550  resdif  5553  f1oco  5554  fvun1  5655  elfvmptrab1  5684  fvreseq  5693  ftpg  5778  f1o2ndf1  6324  spc2ed  6329  smores  6388  nnaord  6605  nnm00  6626  brecop  6722  eroveu  6723  ecopovtrn  6729  ecopovtrng  6732  th3qlem1  6734  th3q  6737  ixpeq2  6809  djuexb  7158  addcmpblnq  7493  mulcmpblnq  7494  mulclnq  7502  dmaddpq  7505  dmmulpq  7506  mulcanenq  7511  distrnqg  7513  ltdcnq  7523  ltexnqq  7534  enq0breq  7562  mulcmpblnq0  7570  mulcanenq0ec  7571  addnnnq0  7575  mulnnnq0  7576  mulclnq0  7578  nqpnq0nq  7579  nqnq0a  7580  nqnq0m  7581  distrnq0  7585  elinp  7600  genpml  7643  genpmu  7644  genprndl  7647  genprndu  7648  addnqprl  7655  addnqpru  7656  distrlem1prl  7708  distrlem1pru  7709  ltsopr  7722  cauappcvgprlemdisj  7777  caucvgprlemdisj  7800  caucvgprprlemdisj  7828  addcmpblnr  7865  addsrpr  7871  mulsrpr  7872  addclsr  7879  addasssrg  7882  0idsr  7893  1idsr  7894  00sr  7895  mulgt0sr  7904  axaddcl  7990  axmulcl  7992  axaddass  7998  axdistr  8000  cnegexlem3  8262  cnegex  8263  apirr  8691  recexaplem2  8738  zletric  9429  zlelttric  9430  difgtsumgt  9455  qaddcl  9769  qmulcl  9771  qreccl  9776  iccss  10076  fzsubel  10195  elfz0add  10255  difelfznle  10270  2ffzeq  10276  fzonmapblen  10324  ubmelfzo  10342  ubmelm1fzo  10368  subfzo0  10384  qletric  10397  qlelttric  10398  adddivflid  10448  mulexp  10736  mulexpzap  10737  leexp1a  10752  faclbnd  10899  wrdeq  11029  ccatcl  11063  swrdsbslen  11133  swrdspsleq  11134  pfxccat1  11167  swrdswrdlem  11169  rexanuz  11349  sqabsadd  11416  sqabssub  11417  abs2dif  11467  rpmincl  11599  xrminrpcl  11635  fsum2dlemstep  11795  fprodeq0  11978  fprod2dlemstep  11983  summodnegmod  12183  dvds2ln  12185  dvdsflip  12212  gcdsupex  12328  gcdsupcl  12329  gcdabs  12359  sqgcd  12400  nnwosdc  12410  lcmabs  12448  lcmgcdlem  12449  lcmgcd  12450  lcmgcdeq  12455  qredeq  12468  cncongr1  12475  cncongr2  12476  hashgcdlem  12610  dvdsprmpweqle  12710  difsqpwdvds  12711  xpsfrnel2  13228  fngsum  13270  igsumvalx  13271  mndissubm  13357  resmhm2  13370  grpissubg  13580  subrngpropd  14028  subrgpropd  14065  tgcl  14586  uncld  14635  innei  14685  cnco  14743  txbas  14780  txbasval  14789  blin2  14954  qtopbasss  15043  lgsmulsqcoprm  15573  gausslemma2dlem1a  15585  lgsquad2lem2  15609  bj-charfunbi  15861  bj-indind  15982