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  2175  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  sseq2  3266  unssin  3464  uneqin  3476  undif3ss  3486  prneimg  3883  ssunieq  3952  iuneq1  4009  iuneq2  4012  copsex2t  4366  soeq2  4442  tpexg  4570  eldifpw  4603  iunpw  4606  peano5  4725  opbrop  4834  xpsspw  4867  coeq1  4917  coeq2  4918  cnveq  4934  dmeq  4961  sotri  5163  elxp4  5255  elxp5  5256  funun  5402  fununfun  5404  fundif  5405  funtp  5414  imain  5443  2elresin  5474  funssxp  5537  fssres  5545  f1co  5590  foun  5638  resdif  5641  f1oco  5642  fvun1  5748  elfvmptrab1  5777  fvreseq  5786  ftpg  5873  f1o2ndf1  6437  spc2ed  6442  fvn0elsupp  6464  smores  6536  nnaord  6755  nnm00  6776  brecop  6872  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  th3q  6887  ixpeq2  6960  djuexb  7348  addcmpblnq  7698  mulcmpblnq  7699  mulclnq  7707  dmaddpq  7710  dmmulpq  7711  mulcanenq  7716  distrnqg  7718  ltdcnq  7728  ltexnqq  7739  enq0breq  7767  mulcmpblnq0  7775  mulcanenq0ec  7776  addnnnq0  7780  mulnnnq0  7781  mulclnq0  7783  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  elinp  7805  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  addnqprl  7860  addnqpru  7861  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  cauappcvgprlemdisj  7982  caucvgprlemdisj  8005  caucvgprprlemdisj  8033  addcmpblnr  8070  addsrpr  8076  mulsrpr  8077  addclsr  8084  addasssrg  8087  0idsr  8098  1idsr  8099  00sr  8100  mulgt0sr  8109  axaddcl  8195  axmulcl  8197  axaddass  8203  axdistr  8205  cnegexlem3  8466  cnegex  8467  apirr  8896  recexaplem2  8943  zletric  9638  zlelttric  9639  difgtsumgt  9664  qaddcl  9985  qmulcl  9987  qreccl  9992  iccss  10293  fzsubel  10415  elfz0add  10476  difelfznle  10491  2ffzeq  10497  fzonmapblen  10548  ubmelfzo  10567  ubmelm1fzo  10593  subfzo0  10610  qletric  10625  qlelttric  10626  adddivflid  10676  mulexp  10964  mulexpzap  10965  leexp1a  10980  faclbnd  11128  wrdeq  11271  ccatcl  11306  swrdsbslen  11383  swrdspsleq  11384  pfxccat1  11419  swrdswrdlem  11421  pfxccatin12lem2a  11444  swrdccatin2  11446  pfxccatin12lem2  11448  swrdccat  11452  reuccatpfxs1  11464  rexanuz  11698  sqabsadd  11765  sqabssub  11766  abs2dif  11816  rpmincl  11948  xrminrpcl  11984  fsum2dlemstep  12145  fprodeq0  12328  fprod2dlemstep  12333  summodnegmod  12533  dvds2ln  12535  dvdsflip  12562  gcdsupex  12678  gcdsupcl  12679  gcdabs  12709  sqgcd  12750  nnwosdc  12760  lcmabs  12798  lcmgcdlem  12799  lcmgcd  12800  lcmgcdeq  12805  qredeq  12818  cncongr1  12825  cncongr2  12826  hashgcdlem  12960  dvdsprmpweqle  13060  difsqpwdvds  13061  xpsfrnel2  13643  fngsum  13685  igsumvalx  13686  mndissubm  13772  resmhm2  13785  grpissubg  13995  subrngpropd  14447  subrgpropd  14484  tgcl  15041  uncld  15090  innei  15140  cnco  15198  txbas  15235  txbasval  15244  blin2  15409  qtopbasss  15498  lgsmulsqcoprm  16031  gausslemma2dlem1a  16043  lgsquad2lem2  16067  umgredgprv  16222  uspgredg2v  16328  usgredg2v  16331  wlkeq  16461  uspgr2wlkeq2  16473  uspgr2wlkeqi  16474  clwwlknonex2  16546  bj-charfunbi  16693  bj-indind  16814