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  995  hban  1596  sbimi  1813  spsbbi  1893  2exeu  2175  cgsex2g  2852  cgsex4g  2853  spc2egv  2909  spc2gv  2910  sseq2  3266  unssin  3464  uneqin  3476  undif3ss  3486  prneimg  3883  ssunieq  3952  iuneq1  4009  iuneq2  4012  copsex2t  4366  soeq2  4442  tpexg  4570  eldifpw  4603  iunpw  4606  peano5  4725  opbrop  4834  xpsspw  4867  coeq1  4917  coeq2  4918  cnveq  4934  dmeq  4961  sotri  5163  elxp4  5255  elxp5  5256  funun  5402  fununfun  5404  fundif  5405  funtp  5414  imain  5443  2elresin  5474  funssxp  5537  fssres  5545  f1co  5590  foun  5638  resdif  5641  f1oco  5642  fvun1  5748  elfvmptrab1  5777  fvreseq  5786  ftpg  5873  f1o2ndf1  6437  spc2ed  6442  fvn0elsupp  6464  smores  6536  nnaord  6755  nnm00  6776  brecop  6872  eroveu  6873  ecopovtrn  6879  ecopovtrng  6882  th3qlem1  6884  th3q  6887  ixpeq2  6960  djuexb  7348  addcmpblnq  7698  mulcmpblnq  7699  mulclnq  7707  dmaddpq  7710  dmmulpq  7711  mulcanenq  7716  distrnqg  7718  ltdcnq  7728  ltexnqq  7739  enq0breq  7767  mulcmpblnq0  7775  mulcanenq0ec  7776  addnnnq0  7780  mulnnnq0  7781  mulclnq0  7783  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  distrnq0  7790  elinp  7805  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  addnqprl  7860  addnqpru  7861  distrlem1prl  7913  distrlem1pru  7914  ltsopr  7927  cauappcvgprlemdisj  7982  caucvgprlemdisj  8005  caucvgprprlemdisj  8033  addcmpblnr  8070  addsrpr  8076  mulsrpr  8077  addclsr  8084  addasssrg  8087  0idsr  8098  1idsr  8099  00sr  8100  mulgt0sr  8109  axaddcl  8195  axmulcl  8197  axaddass  8203  axdistr  8205  cnegexlem3  8467  cnegex  8468  apirr  8897  recexaplem2  8944  zletric  9641  zlelttric  9642  difgtsumgt  9667  qaddcl  9988  qmulcl  9990  qreccl  9995  iccss  10296  fzsubel  10418  elfz0add  10479  difelfznle  10494  2ffzeq  10500  fzonmapblen  10551  ubmelfzo  10570  ubmelm1fzo  10596  subfzo0  10613  qletric  10628  qlelttric  10629  adddivflid  10679  mulexp  10967  mulexpzap  10968  leexp1a  10983  faclbnd  11131  wrdeq  11274  ccatcl  11309  swrdsbslen  11386  swrdspsleq  11387  pfxccat1  11422  swrdswrdlem  11424  pfxccatin12lem2a  11447  swrdccatin2  11449  pfxccatin12lem2  11451  swrdccat  11455  reuccatpfxs1  11467  rexanuz  11702  sqabsadd  11769  sqabssub  11770  abs2dif  11820  rpmincl  11952  xrminrpcl  11988  fsum2dlemstep  12149  fprodeq0  12332  fprod2dlemstep  12337  summodnegmod  12537  dvds2ln  12539  dvdsflip  12566  gcdsupex  12682  gcdsupcl  12683  gcdabs  12713  sqgcd  12754  nnwosdc  12764  lcmabs  12802  lcmgcdlem  12803  lcmgcd  12804  lcmgcdeq  12809  qredeq  12822  cncongr1  12829  cncongr2  12830  hashgcdlem  12964  dvdsprmpweqle  13064  difsqpwdvds  13065  xpsfrnel2  13614  fngsum  13655  igsumvalx  13656  mndissubm  13734  resmhm2  13747  grpissubg  13951  subrngpropd  14466  subrgpropd  14503  tgcl  15059  uncld  15108  innei  15158  cnco  15216  txbas  15253  txbasval  15262  blin2  15427  qtopbasss  15516  lgsmulsqcoprm  16049  gausslemma2dlem1a  16061  lgsquad2lem2  16085  umgredgprv  16240  uspgredg2v  16346  usgredg2v  16349  wlkeq  16479  uspgr2wlkeq2  16491  uspgr2wlkeqi  16492  clwwlknonex2  16564  bj-charfunbi  16721  bj-indind  16842