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  1558  sbimi  1775  spsbbi  1855  2exeu  2130  cgsex2g  2788  cgsex4g  2789  spc2egv  2842  spc2gv  2843  sseq2  3194  unssin  3389  uneqin  3401  undif3ss  3411  prneimg  3789  ssunieq  3857  iuneq1  3914  iuneq2  3917  copsex2t  4263  soeq2  4334  tpexg  4462  eldifpw  4495  iunpw  4498  peano5  4615  opbrop  4723  xpsspw  4756  coeq1  4802  coeq2  4803  cnveq  4819  dmeq  4845  sotri  5042  elxp4  5134  elxp5  5135  funun  5279  funtp  5288  imain  5317  2elresin  5346  funssxp  5404  fssres  5410  f1co  5452  foun  5499  resdif  5502  f1oco  5503  fvun1  5603  elfvmptrab1  5631  fvreseq  5640  ftpg  5721  f1o2ndf1  6254  spc2ed  6259  smores  6318  nnaord  6535  nnm00  6556  brecop  6652  eroveu  6653  ecopovtrn  6659  ecopovtrng  6662  th3qlem1  6664  th3q  6667  ixpeq2  6739  djuexb  7074  addcmpblnq  7397  mulcmpblnq  7398  mulclnq  7406  dmaddpq  7409  dmmulpq  7410  mulcanenq  7415  distrnqg  7417  ltdcnq  7427  ltexnqq  7438  enq0breq  7466  mulcmpblnq0  7474  mulcanenq0ec  7475  addnnnq0  7479  mulnnnq0  7480  mulclnq0  7482  nqpnq0nq  7483  nqnq0a  7484  nqnq0m  7485  distrnq0  7489  elinp  7504  genpml  7547  genpmu  7548  genprndl  7551  genprndu  7552  addnqprl  7559  addnqpru  7560  distrlem1prl  7612  distrlem1pru  7613  ltsopr  7626  cauappcvgprlemdisj  7681  caucvgprlemdisj  7704  caucvgprprlemdisj  7732  addcmpblnr  7769  addsrpr  7775  mulsrpr  7776  addclsr  7783  addasssrg  7786  0idsr  7797  1idsr  7798  00sr  7799  mulgt0sr  7808  axaddcl  7894  axmulcl  7896  axaddass  7902  axdistr  7904  cnegexlem3  8165  cnegex  8166  apirr  8593  recexaplem2  8640  zletric  9328  zlelttric  9329  difgtsumgt  9353  qaddcl  9667  qmulcl  9669  qreccl  9674  iccss  9973  fzsubel  10092  elfz0add  10152  difelfznle  10167  2ffzeq  10173  fzonmapblen  10219  ubmelfzo  10232  ubmelm1fzo  10258  subfzo0  10274  qletric  10276  qlelttric  10277  adddivflid  10325  mulexp  10593  mulexpzap  10594  leexp1a  10609  faclbnd  10756  rexanuz  11032  sqabsadd  11099  sqabssub  11100  abs2dif  11150  rpmincl  11281  xrminrpcl  11317  fsum2dlemstep  11477  fprodeq0  11660  fprod2dlemstep  11665  summodnegmod  11864  dvds2ln  11866  dvdsflip  11892  gcdsupex  11993  gcdsupcl  11994  gcdabs  12024  sqgcd  12065  nnwosdc  12075  lcmabs  12111  lcmgcdlem  12112  lcmgcd  12113  lcmgcdeq  12118  qredeq  12131  cncongr1  12138  cncongr2  12139  hashgcdlem  12273  dvdsprmpweqle  12372  difsqpwdvds  12373  xpsfrnel2  12825  fngsum  12867  igsumvalx  12868  mndissubm  12942  resmhm2  12955  grpissubg  13150  subrngpropd  13580  subrgpropd  13612  tgcl  14041  uncld  14090  innei  14140  cnco  14198  txbas  14235  txbasval  14244  blin2  14409  qtopbasss  14498  lgsmulsqcoprm  14925  bj-charfunbi  15041  bj-indind  15162