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  1547  sbimi  1764  spsbbi  1844  2exeu  2118  cgsex2g  2773  cgsex4g  2774  spc2egv  2827  spc2gv  2828  sseq2  3179  unssin  3374  uneqin  3386  undif3ss  3396  prneimg  3774  ssunieq  3842  iuneq1  3899  iuneq2  3902  copsex2t  4245  soeq2  4316  tpexg  4444  eldifpw  4477  iunpw  4480  peano5  4597  opbrop  4705  xpsspw  4738  coeq1  4784  coeq2  4785  cnveq  4801  dmeq  4827  sotri  5024  elxp4  5116  elxp5  5117  funun  5260  funtp  5269  imain  5298  2elresin  5327  funssxp  5385  fssres  5391  f1co  5433  foun  5480  resdif  5483  f1oco  5484  fvun1  5582  elfvmptrab1  5610  fvreseq  5619  ftpg  5700  f1o2ndf1  6228  spc2ed  6233  smores  6292  nnaord  6509  nnm00  6530  brecop  6624  eroveu  6625  ecopovtrn  6631  ecopovtrng  6634  th3qlem1  6636  th3q  6639  ixpeq2  6711  djuexb  7042  addcmpblnq  7365  mulcmpblnq  7366  mulclnq  7374  dmaddpq  7377  dmmulpq  7378  mulcanenq  7383  distrnqg  7385  ltdcnq  7395  ltexnqq  7406  enq0breq  7434  mulcmpblnq0  7442  mulcanenq0ec  7443  addnnnq0  7447  mulnnnq0  7448  mulclnq0  7450  nqpnq0nq  7451  nqnq0a  7452  nqnq0m  7453  distrnq0  7457  elinp  7472  genpml  7515  genpmu  7516  genprndl  7519  genprndu  7520  addnqprl  7527  addnqpru  7528  distrlem1prl  7580  distrlem1pru  7581  ltsopr  7594  cauappcvgprlemdisj  7649  caucvgprlemdisj  7672  caucvgprprlemdisj  7700  addcmpblnr  7737  addsrpr  7743  mulsrpr  7744  addclsr  7751  addasssrg  7754  0idsr  7765  1idsr  7766  00sr  7767  mulgt0sr  7776  axaddcl  7862  axmulcl  7864  axaddass  7870  axdistr  7872  cnegexlem3  8133  cnegex  8134  apirr  8561  recexaplem2  8608  zletric  9296  zlelttric  9297  difgtsumgt  9321  qaddcl  9634  qmulcl  9636  qreccl  9641  iccss  9940  fzsubel  10059  elfz0add  10119  difelfznle  10134  2ffzeq  10140  fzonmapblen  10186  ubmelfzo  10199  ubmelm1fzo  10225  subfzo0  10241  qletric  10243  qlelttric  10244  adddivflid  10291  mulexp  10558  mulexpzap  10559  leexp1a  10574  faclbnd  10720  rexanuz  10996  sqabsadd  11063  sqabssub  11064  abs2dif  11114  rpmincl  11245  xrminrpcl  11281  fsum2dlemstep  11441  fprodeq0  11624  fprod2dlemstep  11629  summodnegmod  11828  dvds2ln  11830  dvdsflip  11856  gcdsupex  11957  gcdsupcl  11958  gcdabs  11988  sqgcd  12029  nnwosdc  12039  lcmabs  12075  lcmgcdlem  12076  lcmgcd  12077  lcmgcdeq  12082  qredeq  12095  cncongr1  12102  cncongr2  12103  hashgcdlem  12237  dvdsprmpweqle  12335  difsqpwdvds  12336  xpsfrnel2  12764  mndissubm  12865  grpissubg  13052  subrgpropd  13367  tgcl  13534  uncld  13583  innei  13633  cnco  13691  txbas  13728  txbasval  13737  blin2  13902  qtopbasss  13991  lgsmulsqcoprm  14417  bj-charfunbi  14533  bj-indind  14654