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  4387  soeq2  4463  tpexg  4592  eldifpw  4625  iunpw  4628  peano5  4747  opbrop  4856  xpsspw  4889  coeq1  4939  coeq2  4940  cnveq  4956  dmeq  4983  sotri  5186  elxp4  5278  elxp5  5279  funun  5425  fununfun  5427  fundif  5428  funtp  5437  imain  5466  2elresin  5497  funssxp  5560  fssres  5568  f1co  5613  foun  5661  resdif  5664  f1oco  5665  fvun1  5772  elfvmptrab1  5804  fvreseq  5815  ftpg  5902  f1o2ndf1  6468  spc2ed  6473  fvn0elsupp  6495  smores  6568  nnaord  6787  nnm00  6808  brecop  6904  eroveu  6905  ecopovtrn  6911  ecopovtrng  6914  th3qlem1  6916  th3q  6919  ixpeq2  7000  djuexb  7391  addcmpblnq  7741  mulcmpblnq  7742  mulclnq  7750  dmaddpq  7753  dmmulpq  7754  mulcanenq  7759  distrnqg  7761  ltdcnq  7771  ltexnqq  7782  enq0breq  7810  mulcmpblnq0  7818  mulcanenq0ec  7819  addnnnq0  7823  mulnnnq0  7824  mulclnq0  7826  nqpnq0nq  7827  nqnq0a  7828  nqnq0m  7829  distrnq0  7833  elinp  7848  genpml  7891  genpmu  7892  genprndl  7895  genprndu  7896  addnqprl  7903  addnqpru  7904  distrlem1prl  7956  distrlem1pru  7957  ltsopr  7970  cauappcvgprlemdisj  8025  caucvgprlemdisj  8048  caucvgprprlemdisj  8076  addcmpblnr  8113  addsrpr  8119  mulsrpr  8120  addclsr  8127  addasssrg  8130  0idsr  8141  1idsr  8142  00sr  8143  mulgt0sr  8152  axaddcl  8238  axmulcl  8240  axaddass  8246  axdistr  8248  cnegexlem3  8511  cnegex  8512  apirr  8942  recexaplem2  8989  zletric  9698  zlelttric  9699  difgtsumgt  9724  qaddcl  10051  qmulcl  10053  qreccl  10058  iccss  10360  fzsubel  10483  elfz0add  10544  difelfznle  10559  2ffzeq  10565  fzonmapblen  10616  ubmelfzo  10635  ubmelm1fzo  10661  subfzo0  10678  qletric  10693  qlelttric  10694  adddivflid  10748  mulexp  11036  mulexpzap  11037  leexp1a  11052  faclbnd  11201  wrdeq  11348  ccatcl  11383  swrdsbslen  11460  swrdspsleq  11461  pfxccat1  11496  swrdswrdlem  11498  pfxccatin12lem2a  11521  swrdccatin2  11523  pfxccatin12lem2  11525  swrdccat  11529  reuccatpfxs1  11541  rexanuz  11776  sqabsadd  11843  sqabssub  11844  abs2dif  11895  rpmincl  12028  xrminrpcl  12065  fsum2dlemstep  12226  fprodeq0  12409  fprod2dlemstep  12414  summodnegmod  12614  dvds2ln  12616  dvdsflip  12643  gcdsupex  12759  gcdsupcl  12760  gcdabs  12790  sqgcd  12831  nnwosdc  12841  lcmabs  12879  lcmgcdlem  12880  lcmgcd  12881  lcmgcdeq  12886  qredeq  12899  cncongr1  12906  cncongr2  12907  hashgcdlem  13045  dvdsprmpweqle  13145  difsqpwdvds  13146  xpsfrnel2  13726  fngzsum  13767  gzsumvalx  13768  mndissubm  13841  resmhm2  13854  grpissubg  14056  subrngpropd  14633  subrgpropd  14670  tgcl  15323  uncld  15372  innei  15422  cnco  15480  txbas  15517  txbasval  15526  blin2  15691  qtopbasss  15780  lgsmulsqcoprm  16403  gausslemma2dlem1a  16415  lgsquad2lem2  16439  umgredgprv  16594  uspgredg2v  16700  usgredg2v  16703  wlkeq  16833  uspgr2wlkeq2  16845  uspgr2wlkeqi  16846  clwwlknonex2  16918  bj-charfunbi  17075  bj-indind  17196  als-no-surprise  17387  alseu-no-surprise  17419