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  1812  spsbbi  1892  2exeu  2172  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  sseq2  3252  unssin  3448  uneqin  3460  undif3ss  3470  prneimg  3862  ssunieq  3931  iuneq1  3988  iuneq2  3991  copsex2t  4343  soeq2  4419  tpexg  4547  eldifpw  4580  iunpw  4583  peano5  4702  opbrop  4811  xpsspw  4844  coeq1  4893  coeq2  4894  cnveq  4910  dmeq  4937  sotri  5139  elxp4  5231  elxp5  5232  funun  5378  fununfun  5380  fundif  5381  funtp  5390  imain  5419  2elresin  5450  funssxp  5512  fssres  5520  f1co  5563  foun  5611  resdif  5614  f1oco  5615  fvun1  5721  elfvmptrab1  5750  fvreseq  5759  ftpg  5846  f1o2ndf1  6402  spc2ed  6407  fvn0elsupp  6429  smores  6501  nnaord  6720  nnm00  6741  brecop  6837  eroveu  6838  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  th3q  6852  ixpeq2  6924  djuexb  7286  addcmpblnq  7630  mulcmpblnq  7631  mulclnq  7639  dmaddpq  7642  dmmulpq  7643  mulcanenq  7648  distrnqg  7650  ltdcnq  7660  ltexnqq  7671  enq0breq  7699  mulcmpblnq0  7707  mulcanenq0ec  7708  addnnnq0  7712  mulnnnq0  7713  mulclnq0  7715  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  distrnq0  7722  elinp  7737  genpml  7780  genpmu  7781  genprndl  7784  genprndu  7785  addnqprl  7792  addnqpru  7793  distrlem1prl  7845  distrlem1pru  7846  ltsopr  7859  cauappcvgprlemdisj  7914  caucvgprlemdisj  7937  caucvgprprlemdisj  7965  addcmpblnr  8002  addsrpr  8008  mulsrpr  8009  addclsr  8016  addasssrg  8019  0idsr  8030  1idsr  8031  00sr  8032  mulgt0sr  8041  axaddcl  8127  axmulcl  8129  axaddass  8135  axdistr  8137  cnegexlem3  8399  cnegex  8400  apirr  8828  recexaplem2  8875  zletric  9566  zlelttric  9567  difgtsumgt  9592  qaddcl  9912  qmulcl  9914  qreccl  9919  iccss  10219  fzsubel  10338  elfz0add  10398  difelfznle  10413  2ffzeq  10419  fzonmapblen  10470  ubmelfzo  10489  ubmelm1fzo  10515  subfzo0  10532  qletric  10545  qlelttric  10546  adddivflid  10596  mulexp  10884  mulexpzap  10885  leexp1a  10900  faclbnd  11047  wrdeq  11182  ccatcl  11217  swrdsbslen  11294  swrdspsleq  11295  pfxccat1  11330  swrdswrdlem  11332  pfxccatin12lem2a  11355  swrdccatin2  11357  pfxccatin12lem2  11359  swrdccat  11363  reuccatpfxs1  11375  rexanuz  11609  sqabsadd  11676  sqabssub  11677  abs2dif  11727  rpmincl  11859  xrminrpcl  11895  fsum2dlemstep  12056  fprodeq0  12239  fprod2dlemstep  12244  summodnegmod  12444  dvds2ln  12446  dvdsflip  12473  gcdsupex  12589  gcdsupcl  12590  gcdabs  12620  sqgcd  12661  nnwosdc  12671  lcmabs  12709  lcmgcdlem  12710  lcmgcd  12711  lcmgcdeq  12716  qredeq  12729  cncongr1  12736  cncongr2  12737  hashgcdlem  12871  dvdsprmpweqle  12971  difsqpwdvds  12972  xpsfrnel2  13490  fngsum  13532  igsumvalx  13533  mndissubm  13619  resmhm2  13632  grpissubg  13842  subrngpropd  14292  subrgpropd  14329  tgcl  14855  uncld  14904  innei  14954  cnco  15012  txbas  15049  txbasval  15058  blin2  15223  qtopbasss  15312  lgsmulsqcoprm  15845  gausslemma2dlem1a  15857  lgsquad2lem2  15881  umgredgprv  16036  uspgredg2v  16142  usgredg2v  16145  wlkeq  16275  uspgr2wlkeq2  16287  uspgr2wlkeqi  16288  clwwlknonex2  16360  bj-charfunbi  16507  bj-indind  16628