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  7385  addcmpblnq  7735  mulcmpblnq  7736  mulclnq  7744  dmaddpq  7747  dmmulpq  7748  mulcanenq  7753  distrnqg  7755  ltdcnq  7765  ltexnqq  7776  enq0breq  7804  mulcmpblnq0  7812  mulcanenq0ec  7813  addnnnq0  7817  mulnnnq0  7818  mulclnq0  7820  nqpnq0nq  7821  nqnq0a  7822  nqnq0m  7823  distrnq0  7827  elinp  7842  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  addnqprl  7897  addnqpru  7898  distrlem1prl  7950  distrlem1pru  7951  ltsopr  7964  cauappcvgprlemdisj  8019  caucvgprlemdisj  8042  caucvgprprlemdisj  8070  addcmpblnr  8107  addsrpr  8113  mulsrpr  8114  addclsr  8121  addasssrg  8124  0idsr  8135  1idsr  8136  00sr  8137  mulgt0sr  8146  axaddcl  8232  axmulcl  8234  axaddass  8240  axdistr  8242  cnegexlem3  8505  cnegex  8506  apirr  8936  recexaplem2  8983  zletric  9693  zlelttric  9694  difgtsumgt  9719  qaddcl  10045  qmulcl  10047  qreccl  10052  iccss  10354  fzsubel  10477  elfz0add  10538  difelfznle  10553  2ffzeq  10559  fzonmapblen  10610  ubmelfzo  10629  ubmelm1fzo  10655  subfzo0  10672  qletric  10687  qlelttric  10688  adddivflid  10741  mulexp  11029  mulexpzap  11030  leexp1a  11045  faclbnd  11194  wrdeq  11341  ccatcl  11376  swrdsbslen  11453  swrdspsleq  11454  pfxccat1  11489  swrdswrdlem  11491  pfxccatin12lem2a  11514  swrdccatin2  11516  pfxccatin12lem2  11518  swrdccat  11522  reuccatpfxs1  11534  rexanuz  11769  sqabsadd  11836  sqabssub  11837  abs2dif  11888  rpmincl  12021  xrminrpcl  12058  fsum2dlemstep  12219  fprodeq0  12402  fprod2dlemstep  12407  summodnegmod  12607  dvds2ln  12609  dvdsflip  12636  gcdsupex  12752  gcdsupcl  12753  gcdabs  12783  sqgcd  12824  nnwosdc  12834  lcmabs  12872  lcmgcdlem  12873  lcmgcd  12874  lcmgcdeq  12879  qredeq  12892  cncongr1  12899  cncongr2  12900  hashgcdlem  13038  dvdsprmpweqle  13138  difsqpwdvds  13139  xpsfrnel2  13718  fngzsum  13759  gzsumvalx  13760  mndissubm  13833  resmhm2  13846  grpissubg  14048  subrngpropd  14575  subrgpropd  14612  tgcl  15217  uncld  15266  innei  15316  cnco  15374  txbas  15411  txbasval  15420  blin2  15585  qtopbasss  15674  lgsmulsqcoprm  16287  gausslemma2dlem1a  16299  lgsquad2lem2  16323  umgredgprv  16478  uspgredg2v  16584  usgredg2v  16587  wlkeq  16717  uspgr2wlkeq2  16729  uspgr2wlkeqi  16730  clwwlknonex2  16802  bj-charfunbi  16959  bj-indind  17080  als-no-surprise  17269  alseu-no-surprise  17301