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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anim12ci  339  anim1i  340  anim2i  342  anifpdc  999  hban  1600  sbimi  1817  spsbbi  1897  2exeu  2179  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  sseq2  3272  unssin  3470  uneqin  3482  undif3ss  3492  prneimg  3899  ssunieq  3968  iuneq1  4025  iuneq2  4028  copsex2t  4385  soeq2  4461  tpexg  4590  eldifpw  4623  iunpw  4626  peano5  4745  opbrop  4854  xpsspw  4887  coeq1  4937  coeq2  4938  cnveq  4954  dmeq  4981  sotri  5183  elxp4  5275  elxp5  5276  funun  5422  fununfun  5424  fundif  5425  funtp  5434  imain  5463  2elresin  5494  funssxp  5557  fssres  5565  f1co  5610  foun  5658  resdif  5661  f1oco  5662  fvun1  5769  elfvmptrab1  5801  fvreseq  5812  ftpg  5899  f1o2ndf1  6464  spc2ed  6469  fvn0elsupp  6491  smores  6563  nnaord  6782  nnm00  6803  brecop  6899  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  th3q  6914  ixpeq2  6994  djuexb  7384  addcmpblnq  7734  mulcmpblnq  7735  mulclnq  7743  dmaddpq  7746  dmmulpq  7747  mulcanenq  7752  distrnqg  7754  ltdcnq  7764  ltexnqq  7775  enq0breq  7803  mulcmpblnq0  7811  mulcanenq0ec  7812  addnnnq0  7816  mulnnnq0  7817  mulclnq0  7819  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  distrnq0  7826  elinp  7841  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  addnqprl  7896  addnqpru  7897  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  addcmpblnr  8106  addsrpr  8112  mulsrpr  8113  addclsr  8120  addasssrg  8123  0idsr  8134  1idsr  8135  00sr  8136  mulgt0sr  8145  axaddcl  8231  axmulcl  8233  axaddass  8239  axdistr  8241  cnegexlem3  8503  cnegex  8504  apirr  8934  recexaplem2  8981  zletric  9690  zlelttric  9691  difgtsumgt  9716  qaddcl  10037  qmulcl  10039  qreccl  10044  iccss  10345  fzsubel  10468  elfz0add  10529  difelfznle  10544  2ffzeq  10550  fzonmapblen  10601  ubmelfzo  10620  ubmelm1fzo  10646  subfzo0  10663  qletric  10678  qlelttric  10679  adddivflid  10729  mulexp  11017  mulexpzap  11018  leexp1a  11033  faclbnd  11181  wrdeq  11328  ccatcl  11363  swrdsbslen  11440  swrdspsleq  11441  pfxccat1  11476  swrdswrdlem  11478  pfxccatin12lem2a  11501  swrdccatin2  11503  pfxccatin12lem2  11505  swrdccat  11509  reuccatpfxs1  11521  rexanuz  11756  sqabsadd  11823  sqabssub  11824  abs2dif  11874  rpmincl  12006  xrminrpcl  12042  fsum2dlemstep  12203  fprodeq0  12386  fprod2dlemstep  12391  summodnegmod  12591  dvds2ln  12593  dvdsflip  12620  gcdsupex  12736  gcdsupcl  12737  gcdabs  12767  sqgcd  12808  nnwosdc  12818  lcmabs  12856  lcmgcdlem  12857  lcmgcd  12858  lcmgcdeq  12863  qredeq  12876  cncongr1  12883  cncongr2  12884  hashgcdlem  13018  dvdsprmpweqle  13118  difsqpwdvds  13119  xpsfrnel2  13669  fngzsum  13710  gzsumvalx  13711  mndissubm  13784  resmhm2  13797  grpissubg  13999  subrngpropd  14526  subrgpropd  14563  tgcl  15167  uncld  15216  innei  15266  cnco  15324  txbas  15361  txbasval  15370  blin2  15535  qtopbasss  15624  lgsmulsqcoprm  16177  gausslemma2dlem1a  16189  lgsquad2lem2  16213  umgredgprv  16368  uspgredg2v  16474  usgredg2v  16477  wlkeq  16607  uspgr2wlkeq2  16619  uspgr2wlkeqi  16620  clwwlknonex2  16692  bj-charfunbi  16849  bj-indind  16970  als-no-surprise  17159  alseu-no-surprise  17191