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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced 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  3897  ssunieq  3966  iuneq1  4023  iuneq2  4026  copsex2t  4383  soeq2  4459  tpexg  4588  eldifpw  4621  iunpw  4624  peano5  4743  opbrop  4852  xpsspw  4885  coeq1  4935  coeq2  4936  cnveq  4952  dmeq  4979  sotri  5181  elxp4  5273  elxp5  5274  funun  5420  fununfun  5422  fundif  5423  funtp  5432  imain  5461  2elresin  5492  funssxp  5555  fssres  5563  f1co  5608  foun  5656  resdif  5659  f1oco  5660  fvun1  5766  elfvmptrab1  5797  fvreseq  5806  ftpg  5893  f1o2ndf1  6458  spc2ed  6463  fvn0elsupp  6485  smores  6557  nnaord  6776  nnm00  6797  brecop  6893  eroveu  6894  ecopovtrn  6900  ecopovtrng  6903  th3qlem1  6905  th3q  6908  ixpeq2  6988  djuexb  7378  addcmpblnq  7728  mulcmpblnq  7729  mulclnq  7737  dmaddpq  7740  dmmulpq  7741  mulcanenq  7746  distrnqg  7748  ltdcnq  7758  ltexnqq  7769  enq0breq  7797  mulcmpblnq0  7805  mulcanenq0ec  7806  addnnnq0  7810  mulnnnq0  7811  mulclnq0  7813  nqpnq0nq  7814  nqnq0a  7815  nqnq0m  7816  distrnq0  7820  elinp  7835  genpml  7878  genpmu  7879  genprndl  7882  genprndu  7883  addnqprl  7890  addnqpru  7891  distrlem1prl  7943  distrlem1pru  7944  ltsopr  7957  cauappcvgprlemdisj  8012  caucvgprlemdisj  8035  caucvgprprlemdisj  8063  addcmpblnr  8100  addsrpr  8106  mulsrpr  8107  addclsr  8114  addasssrg  8117  0idsr  8128  1idsr  8129  00sr  8130  mulgt0sr  8139  axaddcl  8225  axmulcl  8227  axaddass  8233  axdistr  8235  cnegexlem3  8497  cnegex  8498  apirr  8927  recexaplem2  8974  zletric  9671  zlelttric  9672  difgtsumgt  9697  qaddcl  10018  qmulcl  10020  qreccl  10025  iccss  10326  fzsubel  10449  elfz0add  10510  difelfznle  10525  2ffzeq  10531  fzonmapblen  10582  ubmelfzo  10601  ubmelm1fzo  10627  subfzo0  10644  qletric  10659  qlelttric  10660  adddivflid  10710  mulexp  10998  mulexpzap  10999  leexp1a  11014  faclbnd  11162  wrdeq  11309  ccatcl  11344  swrdsbslen  11421  swrdspsleq  11422  pfxccat1  11457  swrdswrdlem  11459  pfxccatin12lem2a  11482  swrdccatin2  11484  pfxccatin12lem2  11486  swrdccat  11490  reuccatpfxs1  11502  rexanuz  11737  sqabsadd  11804  sqabssub  11805  abs2dif  11855  rpmincl  11987  xrminrpcl  12023  fsum2dlemstep  12184  fprodeq0  12367  fprod2dlemstep  12372  summodnegmod  12572  dvds2ln  12574  dvdsflip  12601  gcdsupex  12717  gcdsupcl  12718  gcdabs  12748  sqgcd  12789  nnwosdc  12799  lcmabs  12837  lcmgcdlem  12838  lcmgcd  12839  lcmgcdeq  12844  qredeq  12857  cncongr1  12864  cncongr2  12865  hashgcdlem  12999  dvdsprmpweqle  13099  difsqpwdvds  13100  xpsfrnel2  13650  fngzsum  13691  gzsumvalx  13692  mndissubm  13765  resmhm2  13778  grpissubg  13980  subrngpropd  14507  subrgpropd  14544  tgcl  15148  uncld  15197  innei  15247  cnco  15305  txbas  15342  txbasval  15351  blin2  15516  qtopbasss  15605  lgsmulsqcoprm  16148  gausslemma2dlem1a  16160  lgsquad2lem2  16184  umgredgprv  16339  uspgredg2v  16445  usgredg2v  16448  wlkeq  16578  uspgr2wlkeq2  16590  uspgr2wlkeqi  16591  clwwlknonex2  16663  bj-charfunbi  16820  bj-indind  16941  als-no-surprise  17121  alseu-no-surprise  17153