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  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  sseq2  3249  unssin  3444  uneqin  3456  undif3ss  3466  prneimg  3855  ssunieq  3924  iuneq1  3981  iuneq2  3984  copsex2t  4335  soeq2  4411  tpexg  4539  eldifpw  4572  iunpw  4575  peano5  4694  opbrop  4803  xpsspw  4836  coeq1  4885  coeq2  4886  cnveq  4902  dmeq  4929  sotri  5130  elxp4  5222  elxp5  5223  funun  5368  fununfun  5370  fundif  5371  funtp  5380  imain  5409  2elresin  5440  funssxp  5501  fssres  5509  f1co  5551  foun  5599  resdif  5602  f1oco  5603  fvun1  5708  elfvmptrab1  5737  fvreseq  5746  ftpg  5833  f1o2ndf1  6388  spc2ed  6393  smores  6453  nnaord  6672  nnm00  6693  brecop  6789  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  th3q  6804  ixpeq2  6876  djuexb  7237  addcmpblnq  7580  mulcmpblnq  7581  mulclnq  7589  dmaddpq  7592  dmmulpq  7593  mulcanenq  7598  distrnqg  7600  ltdcnq  7610  ltexnqq  7621  enq0breq  7649  mulcmpblnq0  7657  mulcanenq0ec  7658  addnnnq0  7662  mulnnnq0  7663  mulclnq0  7665  nqpnq0nq  7666  nqnq0a  7667  nqnq0m  7668  distrnq0  7672  elinp  7687  genpml  7730  genpmu  7731  genprndl  7734  genprndu  7735  addnqprl  7742  addnqpru  7743  distrlem1prl  7795  distrlem1pru  7796  ltsopr  7809  cauappcvgprlemdisj  7864  caucvgprlemdisj  7887  caucvgprprlemdisj  7915  addcmpblnr  7952  addsrpr  7958  mulsrpr  7959  addclsr  7966  addasssrg  7969  0idsr  7980  1idsr  7981  00sr  7982  mulgt0sr  7991  axaddcl  8077  axmulcl  8079  axaddass  8085  axdistr  8087  cnegexlem3  8349  cnegex  8350  apirr  8778  recexaplem2  8825  zletric  9516  zlelttric  9517  difgtsumgt  9542  qaddcl  9862  qmulcl  9864  qreccl  9869  iccss  10169  fzsubel  10288  elfz0add  10348  difelfznle  10363  2ffzeq  10369  fzonmapblen  10419  ubmelfzo  10438  ubmelm1fzo  10464  subfzo0  10481  qletric  10494  qlelttric  10495  adddivflid  10545  mulexp  10833  mulexpzap  10834  leexp1a  10849  faclbnd  10996  wrdeq  11128  ccatcl  11163  swrdsbslen  11240  swrdspsleq  11241  pfxccat1  11276  swrdswrdlem  11278  pfxccatin12lem2a  11301  swrdccatin2  11303  pfxccatin12lem2  11305  swrdccat  11309  reuccatpfxs1  11321  rexanuz  11542  sqabsadd  11609  sqabssub  11610  abs2dif  11660  rpmincl  11792  xrminrpcl  11828  fsum2dlemstep  11988  fprodeq0  12171  fprod2dlemstep  12176  summodnegmod  12376  dvds2ln  12378  dvdsflip  12405  gcdsupex  12521  gcdsupcl  12522  gcdabs  12552  sqgcd  12593  nnwosdc  12603  lcmabs  12641  lcmgcdlem  12642  lcmgcd  12643  lcmgcdeq  12648  qredeq  12661  cncongr1  12668  cncongr2  12669  hashgcdlem  12803  dvdsprmpweqle  12903  difsqpwdvds  12904  xpsfrnel2  13422  fngsum  13464  igsumvalx  13465  mndissubm  13551  resmhm2  13564  grpissubg  13774  subrngpropd  14223  subrgpropd  14260  tgcl  14781  uncld  14830  innei  14880  cnco  14938  txbas  14975  txbasval  14984  blin2  15149  qtopbasss  15238  lgsmulsqcoprm  15768  gausslemma2dlem1a  15780  lgsquad2lem2  15804  umgredgprv  15959  uspgredg2v  16065  usgredg2v  16068  wlkeq  16165  uspgr2wlkeq2  16177  uspgr2wlkeqi  16178  clwwlknonex2  16248  bj-charfunbi  16356  bj-indind  16477