Theorem anim12i 334

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 285	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  anim12ci  335  anim1i  336  anim2i  337  hban  1507  sbimi  1718  spsbbi  1796  2exeu  2065  cgsex2g  2691  cgsex4g  2692  spc2egv  2744  spc2gv  2745  sseq2  3085  unssin  3279  uneqin  3291  undif3ss  3301  prneimg  3665  ssunieq  3733  iuneq1  3790  iuneq2  3793  copsex2t  4125  soeq2  4196  tpexg  4323  eldifpw  4356  iunpw  4359  peano5  4470  opbrop  4576  xpsspw  4609  coeq1  4654  coeq2  4655  cnveq  4671  dmeq  4697  sotri  4890  elxp4  4982  elxp5  4983  funun  5123  funtp  5132  imain  5161  2elresin  5190  funssxp  5248  fssres  5254  f1co  5296  foun  5340  resdif  5343  f1oco  5344  fvun1  5439  elfvmptrab1  5467  fvreseq  5476  ftpg  5556  f1o2ndf1  6076  spc2ed  6081  smores  6140  nnaord  6356  nnm00  6376  brecop  6470  eroveu  6471  ecopovtrn  6477  ecopovtrng  6480  th3qlem1  6482  th3q  6485  ixpeq2  6557  djuexb  6878  addcmpblnq  7116  mulcmpblnq  7117  mulclnq  7125  dmaddpq  7128  dmmulpq  7129  mulcanenq  7134  distrnqg  7136  ltdcnq  7146  ltexnqq  7157  enq0breq  7185  mulcmpblnq0  7193  mulcanenq0ec  7194  addnnnq0  7198  mulnnnq0  7199  mulclnq0  7201  nqpnq0nq  7202  nqnq0a  7203  nqnq0m  7204  distrnq0  7208  elinp  7223  genpml  7266  genpmu  7267  genprndl  7270  genprndu  7271  addnqprl  7278  addnqpru  7279  distrlem1prl  7331  distrlem1pru  7332  ltsopr  7345  cauappcvgprlemdisj  7400  caucvgprlemdisj  7423  caucvgprprlemdisj  7451  addcmpblnr  7475  addsrpr  7481  mulsrpr  7482  addclsr  7489  addasssrg  7492  0idsr  7503  1idsr  7504  00sr  7505  mulgt0sr  7513  axaddcl  7592  axmulcl  7594  axaddass  7600  axdistr  7602  cnegexlem3  7855  cnegex  7856  apirr  8278  recexaplem2  8319  zletric  8995  zlelttric  8996  qaddcl  9322  qmulcl  9324  qreccl  9329  iccss  9610  fzsubel  9726  elfz0add  9786  difelfznle  9798  2ffzeq  9804  fzonmapblen  9850  ubmelfzo  9863  ubmelm1fzo  9889  subfzo0  9905  qletric  9907  qlelttric  9908  adddivflid  9951  mulexp  10218  mulexpzap  10219  leexp1a  10234  faclbnd  10373  rexanuz  10645  sqabsadd  10712  sqabssub  10713  abs2dif  10763  rpmincl  10894  xrminrpcl  10928  fsum2dlemstep  11088  summodnegmod  11365  dvds2ln  11367  dvdsflip  11390  gcdsupex  11487  gcdsupcl  11488  gcdabs  11517  sqgcd  11556  lcmabs  11596  lcmgcdlem  11597  lcmgcd  11598  lcmgcdeq  11603  qredeq  11616  cncongr1  11623  cncongr2  11624  hashgcdlem  11741  tgcl  12069  uncld  12118  innei  12168  cnco  12225  txbas  12262  txbasval  12271  blin2  12414  qtopbasss  12503  bj-indind  12809