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  1545  sbimi  1762  spsbbi  1842  2exeu  2116  cgsex2g  2771  cgsex4g  2772  spc2egv  2825  spc2gv  2826  sseq2  3177  unssin  3372  uneqin  3384  undif3ss  3394  prneimg  3770  ssunieq  3838  iuneq1  3895  iuneq2  3898  copsex2t  4239  soeq2  4310  tpexg  4438  eldifpw  4471  iunpw  4474  peano5  4591  opbrop  4699  xpsspw  4732  coeq1  4777  coeq2  4778  cnveq  4794  dmeq  4820  sotri  5016  elxp4  5108  elxp5  5109  funun  5252  funtp  5261  imain  5290  2elresin  5319  funssxp  5377  fssres  5383  f1co  5425  foun  5472  resdif  5475  f1oco  5476  fvun1  5574  elfvmptrab1  5602  fvreseq  5611  ftpg  5692  f1o2ndf1  6219  spc2ed  6224  smores  6283  nnaord  6500  nnm00  6521  brecop  6615  eroveu  6616  ecopovtrn  6622  ecopovtrng  6625  th3qlem1  6627  th3q  6630  ixpeq2  6702  djuexb  7033  addcmpblnq  7341  mulcmpblnq  7342  mulclnq  7350  dmaddpq  7353  dmmulpq  7354  mulcanenq  7359  distrnqg  7361  ltdcnq  7371  ltexnqq  7382  enq0breq  7410  mulcmpblnq0  7418  mulcanenq0ec  7419  addnnnq0  7423  mulnnnq0  7424  mulclnq0  7426  nqpnq0nq  7427  nqnq0a  7428  nqnq0m  7429  distrnq0  7433  elinp  7448  genpml  7491  genpmu  7492  genprndl  7495  genprndu  7496  addnqprl  7503  addnqpru  7504  distrlem1prl  7556  distrlem1pru  7557  ltsopr  7570  cauappcvgprlemdisj  7625  caucvgprlemdisj  7648  caucvgprprlemdisj  7676  addcmpblnr  7713  addsrpr  7719  mulsrpr  7720  addclsr  7727  addasssrg  7730  0idsr  7741  1idsr  7742  00sr  7743  mulgt0sr  7752  axaddcl  7838  axmulcl  7840  axaddass  7846  axdistr  7848  cnegexlem3  8108  cnegex  8109  apirr  8536  recexaplem2  8582  zletric  9268  zlelttric  9269  difgtsumgt  9293  qaddcl  9606  qmulcl  9608  qreccl  9613  iccss  9910  fzsubel  10028  elfz0add  10088  difelfznle  10103  2ffzeq  10109  fzonmapblen  10155  ubmelfzo  10168  ubmelm1fzo  10194  subfzo0  10210  qletric  10212  qlelttric  10213  adddivflid  10260  mulexp  10527  mulexpzap  10528  leexp1a  10543  faclbnd  10687  rexanuz  10963  sqabsadd  11030  sqabssub  11031  abs2dif  11081  rpmincl  11212  xrminrpcl  11248  fsum2dlemstep  11408  fprodeq0  11591  fprod2dlemstep  11596  summodnegmod  11795  dvds2ln  11797  dvdsflip  11822  gcdsupex  11923  gcdsupcl  11924  gcdabs  11954  sqgcd  11995  nnwosdc  12005  lcmabs  12041  lcmgcdlem  12042  lcmgcd  12043  lcmgcdeq  12048  qredeq  12061  cncongr1  12068  cncongr2  12069  hashgcdlem  12203  dvdsprmpweqle  12301  difsqpwdvds  12302  mndissubm  12726  tgcl  13133  uncld  13182  innei  13232  cnco  13290  txbas  13327  txbasval  13336  blin2  13501  qtopbasss  13590  lgsmulsqcoprm  14016  bj-charfunbi  14121  bj-indind  14242