Theorem anim12i 336

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  anim12ci  337  anim1i  338  anim2i  339  hban  1526  sbimi  1737  spsbbi  1816  2exeu  2091  cgsex2g  2722  cgsex4g  2723  spc2egv  2775  spc2gv  2776  sseq2  3121  unssin  3315  uneqin  3327  undif3ss  3337  prneimg  3701  ssunieq  3769  iuneq1  3826  iuneq2  3829  copsex2t  4167  soeq2  4238  tpexg  4365  eldifpw  4398  iunpw  4401  peano5  4512  opbrop  4618  xpsspw  4651  coeq1  4696  coeq2  4697  cnveq  4713  dmeq  4739  sotri  4934  elxp4  5026  elxp5  5027  funun  5167  funtp  5176  imain  5205  2elresin  5234  funssxp  5292  fssres  5298  f1co  5340  foun  5386  resdif  5389  f1oco  5390  fvun1  5487  elfvmptrab1  5515  fvreseq  5524  ftpg  5604  f1o2ndf1  6125  spc2ed  6130  smores  6189  nnaord  6405  nnm00  6425  brecop  6519  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem1  6531  th3q  6534  ixpeq2  6606  djuexb  6929  addcmpblnq  7175  mulcmpblnq  7176  mulclnq  7184  dmaddpq  7187  dmmulpq  7188  mulcanenq  7193  distrnqg  7195  ltdcnq  7205  ltexnqq  7216  enq0breq  7244  mulcmpblnq0  7252  mulcanenq0ec  7253  addnnnq0  7257  mulnnnq0  7258  mulclnq0  7260  nqpnq0nq  7261  nqnq0a  7262  nqnq0m  7263  distrnq0  7267  elinp  7282  genpml  7325  genpmu  7326  genprndl  7329  genprndu  7330  addnqprl  7337  addnqpru  7338  distrlem1prl  7390  distrlem1pru  7391  ltsopr  7404  cauappcvgprlemdisj  7459  caucvgprlemdisj  7482  caucvgprprlemdisj  7510  addcmpblnr  7547  addsrpr  7553  mulsrpr  7554  addclsr  7561  addasssrg  7564  0idsr  7575  1idsr  7576  00sr  7577  mulgt0sr  7586  axaddcl  7672  axmulcl  7674  axaddass  7680  axdistr  7682  cnegexlem3  7939  cnegex  7940  apirr  8367  recexaplem2  8413  zletric  9098  zlelttric  9099  qaddcl  9427  qmulcl  9429  qreccl  9434  iccss  9724  fzsubel  9840  elfz0add  9900  difelfznle  9912  2ffzeq  9918  fzonmapblen  9964  ubmelfzo  9977  ubmelm1fzo  10003  subfzo0  10019  qletric  10021  qlelttric  10022  adddivflid  10065  mulexp  10332  mulexpzap  10333  leexp1a  10348  faclbnd  10487  rexanuz  10760  sqabsadd  10827  sqabssub  10828  abs2dif  10878  rpmincl  11009  xrminrpcl  11043  fsum2dlemstep  11203  summodnegmod  11524  dvds2ln  11526  dvdsflip  11549  gcdsupex  11646  gcdsupcl  11647  gcdabs  11676  sqgcd  11717  lcmabs  11757  lcmgcdlem  11758  lcmgcd  11759  lcmgcdeq  11764  qredeq  11777  cncongr1  11784  cncongr2  11785  hashgcdlem  11903  tgcl  12233  uncld  12282  innei  12332  cnco  12390  txbas  12427  txbasval  12436  blin2  12601  qtopbasss  12690  bj-indind  13130