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  992  hban  1593  sbimi  1810  spsbbi  1890  2exeu  2170  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  sseq2  3248  unssin  3443  uneqin  3455  undif3ss  3465  prneimg  3851  ssunieq  3920  iuneq1  3977  iuneq2  3980  copsex2t  4330  soeq2  4404  tpexg  4532  eldifpw  4565  iunpw  4568  peano5  4687  opbrop  4795  xpsspw  4828  coeq1  4876  coeq2  4877  cnveq  4893  dmeq  4920  sotri  5120  elxp4  5212  elxp5  5213  funun  5358  fununfun  5360  fundif  5361  funtp  5370  imain  5399  2elresin  5430  funssxp  5489  fssres  5497  f1co  5539  foun  5587  resdif  5590  f1oco  5591  fvun1  5693  elfvmptrab1  5722  fvreseq  5731  ftpg  5816  f1o2ndf1  6364  spc2ed  6369  smores  6428  nnaord  6645  nnm00  6666  brecop  6762  eroveu  6763  ecopovtrn  6769  ecopovtrng  6772  th3qlem1  6774  th3q  6777  ixpeq2  6849  djuexb  7199  addcmpblnq  7542  mulcmpblnq  7543  mulclnq  7551  dmaddpq  7554  dmmulpq  7555  mulcanenq  7560  distrnqg  7562  ltdcnq  7572  ltexnqq  7583  enq0breq  7611  mulcmpblnq0  7619  mulcanenq0ec  7620  addnnnq0  7624  mulnnnq0  7625  mulclnq0  7627  nqpnq0nq  7628  nqnq0a  7629  nqnq0m  7630  distrnq0  7634  elinp  7649  genpml  7692  genpmu  7693  genprndl  7696  genprndu  7697  addnqprl  7704  addnqpru  7705  distrlem1prl  7757  distrlem1pru  7758  ltsopr  7771  cauappcvgprlemdisj  7826  caucvgprlemdisj  7849  caucvgprprlemdisj  7877  addcmpblnr  7914  addsrpr  7920  mulsrpr  7921  addclsr  7928  addasssrg  7931  0idsr  7942  1idsr  7943  00sr  7944  mulgt0sr  7953  axaddcl  8039  axmulcl  8041  axaddass  8047  axdistr  8049  cnegexlem3  8311  cnegex  8312  apirr  8740  recexaplem2  8787  zletric  9478  zlelttric  9479  difgtsumgt  9504  qaddcl  9818  qmulcl  9820  qreccl  9825  iccss  10125  fzsubel  10244  elfz0add  10304  difelfznle  10319  2ffzeq  10325  fzonmapblen  10375  ubmelfzo  10393  ubmelm1fzo  10419  subfzo0  10435  qletric  10448  qlelttric  10449  adddivflid  10499  mulexp  10787  mulexpzap  10788  leexp1a  10803  faclbnd  10950  wrdeq  11080  ccatcl  11114  swrdsbslen  11184  swrdspsleq  11185  pfxccat1  11220  swrdswrdlem  11222  pfxccatin12lem2a  11245  swrdccatin2  11247  pfxccatin12lem2  11249  swrdccat  11253  reuccatpfxs1  11265  rexanuz  11485  sqabsadd  11552  sqabssub  11553  abs2dif  11603  rpmincl  11735  xrminrpcl  11771  fsum2dlemstep  11931  fprodeq0  12114  fprod2dlemstep  12119  summodnegmod  12319  dvds2ln  12321  dvdsflip  12348  gcdsupex  12464  gcdsupcl  12465  gcdabs  12495  sqgcd  12536  nnwosdc  12546  lcmabs  12584  lcmgcdlem  12585  lcmgcd  12586  lcmgcdeq  12591  qredeq  12604  cncongr1  12611  cncongr2  12612  hashgcdlem  12746  dvdsprmpweqle  12846  difsqpwdvds  12847  xpsfrnel2  13365  fngsum  13407  igsumvalx  13408  mndissubm  13494  resmhm2  13507  grpissubg  13717  subrngpropd  14165  subrgpropd  14202  tgcl  14723  uncld  14772  innei  14822  cnco  14880  txbas  14917  txbasval  14926  blin2  15091  qtopbasss  15180  lgsmulsqcoprm  15710  gausslemma2dlem1a  15722  lgsquad2lem2  15746  umgredgprv  15900  uspgredg2v  16004  usgredg2v  16007  bj-charfunbi  16104  bj-indind  16225