Theorem anim12i 614

Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-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 22	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 597	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  anim12ci  615  anim1i  616  anim2i  618  anifp  1071  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  spc2egv  3590  spc2ed  3592  sseq2  4008  uneqin  4278  2reu4lem  4525  2reu4  4526  disjpr2  4717  ssunieq  4947  iuneq1  5013  iuneq2  5016  copsex2t  5492  propeqop  5507  opthhausdorff  5517  opthhausdorff0  5518  iunopeqop  5521  soeq2  5610  opbrop  5772  xpsspw  5808  coeq1  5856  coeq2  5857  cnveq  5872  dmeq  5902  sotri  6126  tz7.7  6388  funun  6592  fununfun  6594  fundif  6595  funprg  6600  funtp  6603  2elresin  6669  funssxp  6744  fssres  6755  f1cof1  6796  f1coOLD  6798  foun  6849  f1un  6851  resdif  6852  f1oco  6854  fvun  6979  elfvmptrab1w  7022  elfvmptrab1  7023  fvn0ssdmfun  7074  dff3  7099  exfo  7104  fprg  7150  ftpg  7151  weisoeq2  7350  oprabv  7466  ndmovdistr  7593  ndmovord  7594  brrpssg  7712  eldifpw  7752  iunpw  7755  epweon  7759  bropfvvvv  8075  f1o2ndf1  8105  poseq  8141  fvn0elsupp  8162  wfrlem5OLD  8310  smores  8349  tz7.49  8442  tz7.49c  8443  oaord  8544  oeeulem  8598  nnaord  8616  brecop  8801  brecop2  8802  eroveu  8803  ecopovtrn  8811  ixpeq2  8902  undifixp  8925  undomOLD  9057  sbthlem8  9087  sbthlem9  9088  unxpdom  9250  isinf  9257  isinfOLD  9258  f1opwfi  9353  fiin  9414  en2lp  9598  inf3lem3  9622  brttrcl  9705  tcmin  9733  djuexb  9901  alephfp  10100  kmlem16  10157  endjudisj  10160  cofsmo  10261  fin23lem28  10332  axdc3lem2  10443  ac6c4  10473  brdom3  10520  brdom5  10521  brdom4  10522  canthp1lem2  10645  finngch  10647  ordpipq  10934  adderpq  10948  mulerpq  10949  lterpq  10962  genpn0  10995  genpnnp  10997  addclprlem2  11009  addcmpblnr  11061  addsrpr  11067  mulsrpr  11068  addclsr  11075  addasssr  11080  distrsr  11083  0idsr  11089  1idsr  11090  00sr  11091  mulgt0sr  11097  axaddf  11137  axaddass  11148  axdistr  11150  cnegex  11392  recextlem2  11842  difgtsumgt  12522  zaddcl  12599  qaddcl  12946  qmulcl  12948  qreccl  12950  xmulgt0  13259  xrsupsslem  13283  xrinfmsslem  13284  supxrpnf  13294  iccss  13389  difreicc  13458  fzadd2  13533  fzsubel  13534  ssfzunsnext  13543  difelfznle  13612  2ffzeq  13619  nelfzo  13634  fzonmapblen  13675  ubmelfzo  13694  ubmelm1fzo  13725  elfznelfzo  13734  subfzo0  13751  adddivflid  13780  modifeq2int  13895  modaddmodup  13896  addmodlteq  13908  fsuppmapnn0fiub  13953  mulexp  14064  mulexpz  14065  leexp1a  14137  faclbnd  14247  hashunx  14343  hashgt23el  14381  wrdeq  14483  ccatcl  14521  swrdnd  14601  swrdnd0  14604  swrdsbslen  14611  swrdspsleq  14612  pfxccat1  14649  swrdswrdlem  14651  pfxccatin12lem2a  14674  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12  14680  swrdccat  14682  reuccatpfxs1  14694  repswswrd  14731  repswccat  14733  cshwidxn  14756  cshweqdif2  14766  2cshwcshw  14773  cshwcshid  14775  cshwcsh2id  14776  f1oun2prg  14865  s2eq2s1eq  14884  s3eqs2s1eq  14886  s3sndisj  14911  s3iunsndisj  14912  sqabsadd  15226  sqabssub  15227  abs2dif  15276  rexanuz  15289  o1of2  15554  o1rlimmul  15560  fsum2dlem  15713  isumltss  15791  fprodser  15890  fprodeq0  15916  fprod2dlem  15921  dvdscmulr  16225  dvdsmulcr  16226  summodnegmod  16227  dvds2ln  16229  dvdsflip  16257  divalglem9  16341  gcdcllem3  16439  gcdaddmlem  16462  gcdabsOLD  16470  sqgcd  16499  lcmcllem  16530  lcmabs  16539  lcmgcdlem  16540  lcmgcd  16541  lcmgcdeq  16546  lcmftp  16570  lcmfunsnlem2lem1  16572  qredeq  16591  cncongr1  16601  cncongr2  16602  isprm7  16642  hashgcdlem  16718  dvdsprmpweqle  16816  difsqpwdvds  16817  prmgaplem4  16984  cshwsidrepsw  17024  setsfun0  17102  setsstruct2  17104  xpsfrnel2  17507  isfunc  17811  tsrss  18539  mndissubm  18685  resmndismnd  18686  resmhm2  18699  submefmnd  18773  sursubmefmnd  18774  injsubmefmnd  18775  grpissubg  19021  gimco  19137  symg2bas  19255  pgrpsubgsymg  19272  symgextf  19280  fvcosymgeq  19292  gsmsymgreqlem1  19293  symgfixf1  19300  efgrelexlema  19612  gsum2dlem1  19833  gsum2dlem2  19834  dvdsr  20169  subrgpropd  20393  islmhm2  20642  psgnghm  21125  psgndiflemB  21145  frlmbas3  21323  frlmphl  21328  islindf4  21385  ressmpladd  21576  ressmplmul  21577  mplind  21623  mpomatmul  21940  mavmul0g  22047  1marepvsma1  22077  mdetdiag  22093  slesolvec  22173  cramerimplem2  22178  cramerimplem3  22179  cramerimp  22180  mat2pmatlin  22229  m2pmfzgsumcl  22242  monmatcollpw  22273  pmatcollpw3lem  22277  pmatcollpwscmatlem1  22283  chpmat1dlem  22329  chfacfisf  22348  chfacfisfcpmat  22349  chfacfpmmulgsum2  22359  tgcl  22464  uncld  22537  innei  22621  cnco  22762  uncmp  22899  txbas  23063  txbasval  23102  tx1stc  23146  fbun  23336  infil  23359  fbunfip  23365  filuni  23381  imaelfm  23447  txflf  23502  tsmsfbas  23624  tsmsxp  23651  blin2  23927  nmhmplusg  24266  qtopbaslem  24267  iccntr  24329  ncvspi  24665  ncvs1  24666  unmbl  25046  volfiniun  25056  mbfi1flimlem  25232  ply1idom  25634  logreclem  26257  relogbcxpb  26282  fsumvma2  26707  chpchtsum  26712  dchrelbas3  26731  dchrmulcl  26742  lgsmulsqcoprm  26836  gausslemma2dlem1a  26858  lgsquad2lem2  26878  dchrisum0fmul  26999  dchrisum0lem1  27009  sltres  27155  nocvxminlem  27269  oldlim  27371  madebdayim  27372  madebdaylemlrcut  27383  ishpg  28000  brcgr  28148  brbtwn2  28153  axcontlem2  28213  uspgredg2v  28471  usgredg2v  28474  usgr2v1e2w  28499  nb3gr2nb  28631  cusgredg  28671  cplgr3v  28682  cusgrop  28685  rusgr1vtx  28835  iswlkg  28860  wlkeq  28881  wlk1walk  28886  uspgr2wlkeq2  28894  uspgr2wlkeqi  28895  crctcshwlkn0lem3  29056  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  wspthneq1eq2  29104  wwlksnextinj  29143  2wlkdlem7  29176  2wlkdlem8  29177  2pthon3v  29187  s3wwlks2on  29200  elwwlks2  29210  elwspths2spth  29211  rusgrnumwwlks  29218  clwlkclwwlklem2a  29241  clwlkclwwlklem3  29244  clwlkclwwlkf1lem2  29248  clwlkclwwlkf1  29253  clwwlknonex2  29352  3wlkdlem3  29404  uhgr3cyclex  29425  cusconngr  29434  eupth0  29457  frgr3v  29518  1to3vfriswmgr  29523  4cycl2v2nb  29532  frgrnbnb  29536  frgrncvvdeq  29552  frgrwopreglem4a  29553  frgrwopreglem5a  29554  frgrwopreglem4  29558  frgrwopreglem5  29564  frgrhash2wsp  29575  numclwwlk1lem2foa  29597  numclwwlk2  29624  blocni  30046  hvsub4  30278  shscli  30558  shscom  30560  spanunsni  30820  spanpr  30821  5oalem2  30896  5oalem3  30897  5oalem5  30899  3oalem1  30903  hoscl  30986  hoadddi  31044  hoadddir  31045  hosub4  31054  lnophsi  31242  hmops  31261  hmopm  31262  adjadd  31334  leop2  31365  leopadd  31373  leopmuli  31374  pjclem4  31440  pj3si  31448  mdslmd1lem2  31567  mdslmd3i  31573  atomli  31623  atcvatlem  31626  chirredlem3  31633  chirredi  31635  atcvat3i  31637  mdsymlem1  31644  mdsymlem5  31648  cdjreui  31673  cdj3i  31682  addltmulALT  31687  hashxpe  32007  mndpluscn  32895  sxbrsigalem5  33276  probfinmeasbALTV  33417  bnj545  33895  bnj546  33896  bnj557  33901  bnj570  33905  bnj594  33912  bnj1001  33959  bnj1118  33984  txpconn  34212  cvmlift2lem10  34292  gonar  34375  lediv2aALT  34651  altopeq12  34923  altxpsspw  34938  funtransport  34992  neibastop1  35233  filnetlem3  35254  lukshef-ax2  35289  arg-ax  35290  nndivsub  35331  bj-nnftht  35608  bj-nnfan  35615  bj-nnfor  35617  copsex2b  36010  isbasisrelowllem1  36225  isbasisrelowllem2  36226  icoreclin  36227  relowlssretop  36233  rdgeqoa  36240  fvineqsnf1  36280  wl-ax11-lem2  36437  matunitlindflem1  36473  matunitlindflem2  36474  poimirlem4  36481  poimirlem26  36503  poimirlem29  36506  poimirlem30  36507  heicant  36512  mblfinlem1  36514  ismblfin  36518  itg2addnclem  36528  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  prdstotbnd  36651  heibor1lem  36666  isdrngo2  36815  divrngidl  36885  pridlc3  36930  linepsubN  38612  pmapsub  38628  elpaddri  38662  paddasslem14  38693  pmapjoin  38712  dvhfvadd  39951  dvhvaddcomN  39956  andiff  41008  imacrhmcl  41087  rimco  41091  rmxynorm  41643  monotoddzzfi  41667  acongtr  41703  mpaaeu  41878  oaltublim  42026  omord2lim  42036  cantnftermord  42056  dflim5  42065  omabs2  42068  tfsconcat0i  42081  ofoafo  42092  naddcnff  42098  oaun3lem1  42110  oaun3lem2  42111  pr2cv  42285  brfvrcld2  42429  rfovcnvf1od  42741  ismnushort  43046  nzin  43063  pm10.14  43104  disjrnmpt2  43872  liminfvalxr  44486  etransclem38  44975  cfsetsnfsetf1  45756  tz6.12-afv2  45935  2elfz2melfz  46013  fz0addge0  46014  2ffzoeq  46023  icceuelpartlem  46090  icceuelpart  46091  ich2exprop  46126  sqrtpwpw2p  46193  fmtnoprmfac1lem  46219  fmtnoprmfac1  46220  lighneallem2  46261  divgcdoddALTV  46337  gbowpos  46414  gbowgt5  46417  gboge9  46419  nnsum3primesgbe  46447  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  isupwlkg  46502  rabsubmgmd  46548  resmgmhm2  46556  ismhm0  46562  mhmismgmhm  46563  isrnghmmul  46677  c0ghm  46696  rhmisrnghm  46708  subrngpropd  46732  rnghmsubcsetclem2  46828  rngcinv  46833  rngcinvALTV  46845  rhmsubcsetclem2  46874  rhmsubcrngclem2  46880  ringcinv  46884  ringcinvALTV  46908  srhmsubc  46928  srhmsubcALTV  46946  mapprop  46976  zlmodzxzadd  46988  domnmsuppn0  46999  mndpfsupp  47006  ply1mulgsumlem2  47022  lincsum  47064  lincsumcl  47066  lincscmcl  47067  isldepslvec2  47120  modn0mul  47160  digexp  47247  rrx2pnecoorneor  47355  rrx2pnedifcoorneorr  47357  rrx2xpref1o  47358  ehl2eudis0lt  47366  rrx2linest  47382  line2x  47394  itsclc0yqsollem2  47403  seppsepf  47515  thincn0eu  47606