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  2774  cgsex4g  2775  spc2egv  2828  spc2gv  2829  sseq2  3180  unssin  3375  uneqin  3387  undif3ss  3397  prneimg  3775  ssunieq  3843  iuneq1  3900  iuneq2  3903  copsex2t  4246  soeq2  4317  tpexg  4445  eldifpw  4478  iunpw  4481  peano5  4598  opbrop  4706  xpsspw  4739  coeq1  4785  coeq2  4786  cnveq  4802  dmeq  4828  sotri  5025  elxp4  5117  elxp5  5118  funun  5261  funtp  5270  imain  5299  2elresin  5328  funssxp  5386  fssres  5392  f1co  5434  foun  5481  resdif  5484  f1oco  5485  fvun1  5583  elfvmptrab1  5611  fvreseq  5620  ftpg  5701  f1o2ndf1  6229  spc2ed  6234  smores  6293  nnaord  6510  nnm00  6531  brecop  6625  eroveu  6626  ecopovtrn  6632  ecopovtrng  6635  th3qlem1  6637  th3q  6640  ixpeq2  6712  djuexb  7043  addcmpblnq  7366  mulcmpblnq  7367  mulclnq  7375  dmaddpq  7378  dmmulpq  7379  mulcanenq  7384  distrnqg  7386  ltdcnq  7396  ltexnqq  7407  enq0breq  7435  mulcmpblnq0  7443  mulcanenq0ec  7444  addnnnq0  7448  mulnnnq0  7449  mulclnq0  7451  nqpnq0nq  7452  nqnq0a  7453  nqnq0m  7454  distrnq0  7458  elinp  7473  genpml  7516  genpmu  7517  genprndl  7520  genprndu  7521  addnqprl  7528  addnqpru  7529  distrlem1prl  7581  distrlem1pru  7582  ltsopr  7595  cauappcvgprlemdisj  7650  caucvgprlemdisj  7673  caucvgprprlemdisj  7701  addcmpblnr  7738  addsrpr  7744  mulsrpr  7745  addclsr  7752  addasssrg  7755  0idsr  7766  1idsr  7767  00sr  7768  mulgt0sr  7777  axaddcl  7863  axmulcl  7865  axaddass  7871  axdistr  7873  cnegexlem3  8134  cnegex  8135  apirr  8562  recexaplem2  8609  zletric  9297  zlelttric  9298  difgtsumgt  9322  qaddcl  9635  qmulcl  9637  qreccl  9642  iccss  9941  fzsubel  10060  elfz0add  10120  difelfznle  10135  2ffzeq  10141  fzonmapblen  10187  ubmelfzo  10200  ubmelm1fzo  10226  subfzo0  10242  qletric  10244  qlelttric  10245  adddivflid  10292  mulexp  10559  mulexpzap  10560  leexp1a  10575  faclbnd  10721  rexanuz  10997  sqabsadd  11064  sqabssub  11065  abs2dif  11115  rpmincl  11246  xrminrpcl  11282  fsum2dlemstep  11442  fprodeq0  11625  fprod2dlemstep  11630  summodnegmod  11829  dvds2ln  11831  dvdsflip  11857  gcdsupex  11958  gcdsupcl  11959  gcdabs  11989  sqgcd  12030  nnwosdc  12040  lcmabs  12076  lcmgcdlem  12077  lcmgcd  12078  lcmgcdeq  12083  qredeq  12096  cncongr1  12103  cncongr2  12104  hashgcdlem  12238  dvdsprmpweqle  12336  difsqpwdvds  12337  xpsfrnel2  12765  mndissubm  12866  grpissubg  13054  subrgpropd  13369  tgcl  13567  uncld  13616  innei  13666  cnco  13724  txbas  13761  txbasval  13770  blin2  13935  qtopbasss  14024  lgsmulsqcoprm  14450  bj-charfunbi  14566  bj-indind  14687