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  6567  nnaord  6786  nnm00  6807  brecop  6903  eroveu  6904  ecopovtrn  6910  ecopovtrng  6913  th3qlem1  6915  th3q  6918  ixpeq2  6999  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  9700  zlelttric  9701  difgtsumgt  9726  qaddcl  10052  qmulcl  10054  qreccl  10059  iccss  10361  fzsubel  10484  elfz0add  10545  difelfznle  10560  2ffzeq  10566  fzonmapblen  10617  ubmelfzo  10636  ubmelm1fzo  10662  subfzo0  10679  qletric  10694  qlelttric  10695  adddivflid  10749  mulexp  11037  mulexpzap  11038  leexp1a  11053  faclbnd  11202  wrdeq  11349  ccatcl  11384  swrdsbslen  11461  swrdspsleq  11462  pfxccat1  11497  swrdswrdlem  11499  pfxccatin12lem2a  11522  swrdccatin2  11524  pfxccatin12lem2  11526  swrdccat  11530  reuccatpfxs1  11542  rexanuz  11777  sqabsadd  11844  sqabssub  11845  abs2dif  11896  rpmincl  12029  xrminrpcl  12066  fsum2dlemstep  12227  fprodeq0  12410  fprod2dlemstep  12415  summodnegmod  12615  dvds2ln  12617  dvdsflip  12644  gcdsupex  12760  gcdsupcl  12761  gcdabs  12791  sqgcd  12832  nnwosdc  12842  lcmabs  12880  lcmgcdlem  12881  lcmgcd  12882  lcmgcdeq  12887  qredeq  12900  cncongr1  12907  cncongr2  12908  hashgcdlem  13046  dvdsprmpweqle  13146  difsqpwdvds  13147  xpsfrnel2  13727  fngzsum  13768  gzsumvalx  13769  mndissubm  13842  resmhm2  13855  grpissubg  14057  subrngpropd  14634  subrgpropd  14671  tgcl  15302  uncld  15351  innei  15401  cnco  15459  txbas  15496  txbasval  15505  blin2  15670  qtopbasss  15759  lgsmulsqcoprm  16382  gausslemma2dlem1a  16394  lgsquad2lem2  16418  umgredgprv  16573  uspgredg2v  16679  usgredg2v  16682  wlkeq  16812  uspgr2wlkeq2  16824  uspgr2wlkeqi  16825  clwwlknonex2  16897  bj-charfunbi  17054  bj-indind  17175  als-no-surprise  17366  alseu-no-surprise  17398