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  1561  sbimi  1778  spsbbi  1858  2exeu  2137  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  sseq2  3208  unssin  3403  uneqin  3415  undif3ss  3425  prneimg  3805  ssunieq  3873  iuneq1  3930  iuneq2  3933  copsex2t  4279  soeq2  4352  tpexg  4480  eldifpw  4513  iunpw  4516  peano5  4635  opbrop  4743  xpsspw  4776  coeq1  4824  coeq2  4825  cnveq  4841  dmeq  4867  sotri  5066  elxp4  5158  elxp5  5159  funun  5303  funtp  5312  imain  5341  2elresin  5372  funssxp  5430  fssres  5436  f1co  5478  foun  5526  resdif  5529  f1oco  5530  fvun1  5630  elfvmptrab1  5659  fvreseq  5668  ftpg  5749  f1o2ndf1  6295  spc2ed  6300  smores  6359  nnaord  6576  nnm00  6597  brecop  6693  eroveu  6694  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  th3q  6708  ixpeq2  6780  djuexb  7119  addcmpblnq  7451  mulcmpblnq  7452  mulclnq  7460  dmaddpq  7463  dmmulpq  7464  mulcanenq  7469  distrnqg  7471  ltdcnq  7481  ltexnqq  7492  enq0breq  7520  mulcmpblnq0  7528  mulcanenq0ec  7529  addnnnq0  7533  mulnnnq0  7534  mulclnq0  7536  nqpnq0nq  7537  nqnq0a  7538  nqnq0m  7539  distrnq0  7543  elinp  7558  genpml  7601  genpmu  7602  genprndl  7605  genprndu  7606  addnqprl  7613  addnqpru  7614  distrlem1prl  7666  distrlem1pru  7667  ltsopr  7680  cauappcvgprlemdisj  7735  caucvgprlemdisj  7758  caucvgprprlemdisj  7786  addcmpblnr  7823  addsrpr  7829  mulsrpr  7830  addclsr  7837  addasssrg  7840  0idsr  7851  1idsr  7852  00sr  7853  mulgt0sr  7862  axaddcl  7948  axmulcl  7950  axaddass  7956  axdistr  7958  cnegexlem3  8220  cnegex  8221  apirr  8649  recexaplem2  8696  zletric  9387  zlelttric  9388  difgtsumgt  9412  qaddcl  9726  qmulcl  9728  qreccl  9733  iccss  10033  fzsubel  10152  elfz0add  10212  difelfznle  10227  2ffzeq  10233  fzonmapblen  10280  ubmelfzo  10293  ubmelm1fzo  10319  subfzo0  10335  qletric  10348  qlelttric  10349  adddivflid  10399  mulexp  10687  mulexpzap  10688  leexp1a  10703  faclbnd  10850  wrdeq  10974  rexanuz  11170  sqabsadd  11237  sqabssub  11238  abs2dif  11288  rpmincl  11420  xrminrpcl  11456  fsum2dlemstep  11616  fprodeq0  11799  fprod2dlemstep  11804  summodnegmod  12004  dvds2ln  12006  dvdsflip  12033  gcdsupex  12149  gcdsupcl  12150  gcdabs  12180  sqgcd  12221  nnwosdc  12231  lcmabs  12269  lcmgcdlem  12270  lcmgcd  12271  lcmgcdeq  12276  qredeq  12289  cncongr1  12296  cncongr2  12297  hashgcdlem  12431  dvdsprmpweqle  12531  difsqpwdvds  12532  xpsfrnel2  13048  fngsum  13090  igsumvalx  13091  mndissubm  13177  resmhm2  13190  grpissubg  13400  subrngpropd  13848  subrgpropd  13885  tgcl  14384  uncld  14433  innei  14483  cnco  14541  txbas  14578  txbasval  14587  blin2  14752  qtopbasss  14841  lgsmulsqcoprm  15371  gausslemma2dlem1a  15383  lgsquad2lem2  15407  bj-charfunbi  15541  bj-indind  15662