Theorem anim12i 624

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 23	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 607	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anim12ci  625  anim1i  626  anim2i  628  anifp  1086  cgsex2g  3502  cgsex4g  3503  spc2egv  3561  spc2ed  3563  uneqin  4244  2reu4lem  4480  2reu4  4481  disjpr2  4675  ssunieq  4904  iuneq1  4968  iuneq2  4971  copsex2t  5465  propeqop  5480  opthhausdorff  5490  opthhausdorff0  5491  iunopeqop  5494  iunopeqopOLD  5495  soeq2  5581  opbrop  5749  xpsspw  5786  coeq1  5833  coeq2  5834  cnveq  5849  dmeq  5883  sotri  6117  tz7.7  6375  funun  6571  fununfun  6573  fundif  6574  funprg  6579  funtp  6582  2elresin  6646  funssxp  6724  fssres  6734  f1cof1  6776  foun  6829  f1un  6831  resdif  6832  f1oco  6834  fvun  6961  elfvmptrab1w  7007  elfvmptrab1  7008  fvn0ssdmfun  7059  dff3  7085  exfo  7090  fprg  7142  ftpg  7143  f1ounsn  7260  weisoeq2  7344  oprabv  7460  ndmovdistr  7589  ndmovord  7590  brrpssg  7712  eldifpw  7755  iunpw  7758  epweon  7762  bropfvvvv  8075  f1o2ndf1  8105  poseq  8142  fvn0elsupp  8164  smores  8327  tz7.49  8420  tz7.49c  8421  oaord  8520  oeeulem  8575  nnaord  8593  brecop  8796  brecop2  8797  eroveu  8798  ecopovtrn  8806  ixpeq2  8897  undifixp  8920  sbthlem8  9070  sbthlem9  9071  unxpdom  9207  isinf  9213  f1opwfi  9301  fiin  9370  en2lp  9563  inf3lem3  9587  brttrcl  9670  tcmin  9696  djuexb  9883  alephfp  10080  kmlem16  10137  endjudisj  10140  cofsmo  10241  fin23lem28  10312  axdc3lem2  10423  ac6c4  10453  brdom3  10500  brdom5  10501  brdom4  10502  canthp1lem2  10626  finngch  10628  ordpipq  10915  adderpq  10929  mulerpq  10930  lterpq  10943  genpn0  10976  genpnnp  10978  addclprlem2  10990  addcmpblnr  11042  addsrpr  11048  mulsrpr  11049  addclsr  11056  addasssr  11061  distrsr  11064  0idsr  11070  1idsr  11071  00sr  11072  mulgt0sr  11078  axaddf  11118  axaddass  11129  axdistr  11131  cnegex  11379  recextlem2  11833  difgtsumgt  12545  zaddcl  12622  qaddcl  12977  qmulcl  12979  qreccl  12981  xmulgt0  13297  xrsupsslem  13321  xrinfmsslem  13322  supxrpnf  13332  iccss  13429  difreicc  13499  fzadd2  13575  fzsubel  13576  ssfzunsnext  13585  difelfznle  13658  2ffzeq  13665  nelfzo  13681  fzonmapblen  13725  ubmelfzo  13747  ubmelm1fzo  13780  elfznelfzo  13790  subfzo0  13809  adddivflid  13839  modaddid  13931  modifeq2int  13957  modaddmodup  13958  addmodlteq  13970  fsuppmapnn0fiub  14015  mulexp  14125  mulexpz  14126  leexp1a  14199  faclbnd  14314  hashunx  14410  hashgt23el  14449  wrdeq  14561  ccatcl  14599  swrdnd  14680  swrdnd0  14683  swrdsbslen  14690  swrdspsleq  14691  pfxccat1  14727  swrdswrdlem  14729  pfxccatin12lem2a  14752  swrdccatin2  14754  pfxccatin12lem2  14756  pfxccatin12  14758  swrdccat  14760  reuccatpfxs1  14772  repswswrd  14809  repswccat  14811  cshwidxn  14834  cshweqdif2  14844  2cshwcshw  14850  cshwcshid  14852  cshwcsh2id  14853  f1oun2prg  14942  s2eq2s1eq  14961  s3eqs2s1eq  14963  s3sndisj  14992  s3iunsndisj  14993  sqabsadd  15321  sqabssub  15322  abs2dif  15372  rexanuz  15385  o1of2  15652  o1rlimmul  15658  fsum2dlem  15809  isumltss  15890  fprodser  15991  fprodeq0  16017  fprod2dlem  16022  dvdscmulr  16330  dvdsmulcr  16331  summodnegmod  16332  difmod0  16333  dvds2ln  16335  dvdsflip  16363  divalglem9  16447  gcdcllem3  16547  gcdaddmlem  16570  sqgcd  16608  lcmcllem  16642  lcmabs  16651  lcmgcdlem  16652  lcmgcd  16653  lcmgcdeq  16658  lcmftp  16682  lcmfunsnlem2lem1  16684  qredeq  16703  cncongr1  16713  cncongr2  16714  isprm7  16755  hashgcdlem  16835  dvdsprmpweqle  16934  difsqpwdvds  16935  prmgaplem4  17102  cshwsidrepsw  17141  setsfun0  17220  setsstruct2  17222  xpsfrnel2  17606  isfunc  17909  tsrss  18633  chnpof1  18674  rabsubmgmd  18750  resmgmhm2  18758  mndpfsupp  18813  ismhm0  18836  mhmismgmhm  18837  mndissubm  18853  resmndismnd  18854  resmhm2  18868  submefmnd  18942  sursubmefmnd  18943  injsubmefmnd  18944  grpissubg  19201  gimco  19326  symg2bas  19451  pgrpsubgsymg  19467  symgextf  19475  fvcosymgeq  19487  gsmsymgreqlem1  19488  symgfixf1  19495  efgrelexlema  19807  gsum2dlem1  20028  gsum2dlem2  20029  dvdsr  20432  isrnghmmul  20512  c0ghm  20531  rhmisrnghm  20550  subrngpropd  20641  subrgpropd  20681  rnghmsubcsetclem2  20705  rngcinv  20710  rhmsubcsetclem2  20734  rhmsubcrngclem2  20740  ringcinv  20744  srhmsubc  20753  islmhm2  21125  unichnlidl  21328  psgnghm  21687  psgndiflemB  21707  frlmbas3  21883  frlmphl  21888  islindf4  21945  ressmpladd  22136  ressmplmul  22137  mplind  22178  mpomatmul  22560  mavmul0g  22667  1marepvsma1  22697  mdetdiag  22713  slesolvec  22793  cramerimplem2  22798  cramerimplem3  22799  cramerimp  22800  mat2pmatlin  22849  m2pmfzgsumcl  22862  monmatcollpw  22893  pmatcollpw3lem  22897  pmatcollpwscmatlem1  22903  chpmat1dlem  22949  chfacfisf  22968  chfacfisfcpmat  22969  chfacfpmmulgsum2  22979  tgcl  23083  uncld  23155  innei  23239  cnco  23380  uncmp  23517  txbas  23681  txbasval  23720  tx1stc  23764  fbun  23954  infil  23977  fbunfip  23983  filuni  23999  imaelfm  24065  txflf  24120  tsmsfbas  24242  tsmsxp  24269  blin2  24543  nmhmplusg  24871  qtopbaslem  24872  iccntr  24936  ncvspi  25272  ncvs1  25273  unmbl  25653  volfiniun  25663  mbfi1flimlem  25838  ply1idom  26239  logreclem  26881  relogbcxpb  26906  fsumvma2  27332  chpchtsum  27337  dchrelbas3  27356  dchrmulcl  27367  lgsmulsqcoprm  27461  gausslemma2dlem1a  27483  lgsquad2lem2  27503  dchrisum0fmul  27624  dchrisum0lem1  27634  ltsres  27780  nocvxminlem  27901  oldlim  28034  madebdayim  28035  madebdaylemlrcut  28046  readdscl  28646  remulscl  28649  ishpg  28986  brcgr  29155  brbtwn2  29160  axcontlem2  29220  uspgredg2v  29479  usgredg2v  29482  usgr2v1e2w  29507  nb3gr2nb  29639  cusgredg  29679  cplgr3v  29690  cusgrop  29693  rusgr1vtx  29843  iswlkg  29868  wlkeq  29888  wlk1walk  29893  uspgr2wlkeq2  29901  uspgr2wlkeqi  29902  cyclnumvtx  30054  crctcshwlkn0lem3  30066  crctcshwlkn0lem4  30067  crctcshwlkn0lem5  30068  wspthneq1eq2  30114  wwlksnextinj  30153  2wlkdlem7  30186  2wlkdlem8  30187  2pthon3v  30197  s3wwlks2on  30210  sps3wwlks2on  30211  elwwlks2  30223  elwspths2spth  30224  rusgrnumwwlks  30231  clwlkclwwlklem2a  30254  clwlkclwwlklem3  30257  clwlkclwwlkf1lem2  30261  clwlkclwwlkf1  30266  clwwlknonex2  30365  3wlkdlem3  30417  uhgr3cyclex  30438  cusconngr  30447  eupth0  30470  frgr3v  30531  1to3vfriswmgr  30536  4cycl2v2nb  30545  frgrnbnb  30549  frgrncvvdeq  30565  frgrwopreglem4a  30566  frgrwopreglem5a  30567  frgrwopreglem4  30571  frgrwopreglem5  30577  frgrhash2wsp  30588  numclwwlk1lem2foa  30610  numclwwlk2  30637  blocni  31062  hvsub4  31294  shscli  31574  shscom  31576  spanunsni  31836  spanpr  31837  5oalem2  31912  5oalem3  31913  5oalem5  31915  3oalem1  31919  hoscl  32002  hoadddi  32060  hoadddir  32061  hosub4  32070  lnophsi  32258  hmops  32277  hmopm  32278  adjadd  32350  leop2  32381  leopadd  32389  leopmuli  32390  pjclem4  32456  pj3si  32464  mdslmd1lem2  32583  mdslmd3i  32589  atomli  32639  atcvatlem  32642  chirredlem3  32649  chirredi  32651  atcvat3i  32653  mdsymlem1  32660  mdsymlem5  32664  cdjreui  32689  cdj3i  32698  addltmulALT  32703  hashxpe  33060  domnmuln0rd  33505  mndpluscn  34228  sxbrsigalem5  34590  probfinmeasbALTV  34731  bnj545  35195  bnj546  35196  bnj557  35201  bnj570  35205  bnj594  35212  bnj1001  35259  bnj1118  35284  txpconn  35590  cvmlift2lem10  35670  gonar  35753  lediv2aALT  36035  altopeq12  36320  altxpsspw  36335  funtransport  36389  neibastop1  36727  filnetlem3  36748  lukshef-ax2  36783  arg-ax  36784  nndivsub  36825  bj-nnfan  37236  bj-nnfor  37238  cgsex2gd  37636  copsex2b  37639  isbasisrelowllem1  37856  isbasisrelowllem2  37857  icoreclin  37858  relowlssretop  37864  rdgeqoa  37871  fvineqsnf1  37911  matunitlindflem1  38122  matunitlindflem2  38123  poimirlem4  38130  poimirlem26  38152  poimirlem29  38155  poimirlem30  38156  heicant  38161  mblfinlem1  38163  ismblfin  38167  itg2addnclem  38177  ftc1anclem6  38204  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  prdstotbnd  38300  heibor1lem  38315  isdrngo2  38464  divrngidl  38534  pridlc3  38579  eldisjdmqsim  39323  linepsubN  40383  pmapsub  40399  elpaddri  40433  paddasslem14  40464  pmapjoin  40483  dvhfvadd  41722  dvhvaddcomN  41727  bcle2d  42803  imacrhmcl  43143  rimco  43144  rmxynorm  43502  monotoddzzfi  43526  acongtr  43562  mpaaeu  43734  oaltublim  43874  omord2lim  43884  cantnftermord  43904  dflim5  43913  omabs2  43916  tfsconcat0i  43929  ofoafo  43940  naddcnff  43946  oaun3lem1  43958  oaun3lem2  43959  pr2cv  44131  brfvrcld2  44275  rfovcnvf1od  44587  ismnushort  44870  nzin  44887  pm10.14  44928  disjrnmpt2  45765  liminfvalxr  46356  etransclem38  46845  cfsetsnfsetf1  47652  tz6.12-afv2  47833  2elfz2melfz  47911  fz0addge0  47912  2ffzoeq  47921  difltmodne  47941  modn0mul  47956  mod2addne  47963  icceuelpartlem  48040  icceuelpart  48041  ich2exprop  48076  sqrtpwpw2p  48146  fmtnoprmfac1lem  48172  fmtnoprmfac1  48173  lighneallem2  48214  divgcdoddALTV  48303  gbowpos  48380  gbowgt5  48383  gboge9  48385  nnsum3primesgbe  48413  bgoldbtbndlem2  48427  bgoldbtbndlem3  48428  isuspgrim  48517  clnbgrgrimlem  48554  clnbgrgrim  48555  isgrtri  48564  isubgr3stgrlem4  48590  grlimgrtri  48624  grlictr  48636  gpgedgvtx0  48682  gpgedg2iv  48688  gpg5nbgrvtx03star  48701  gpg5nbgr3star  48702  pgnbgreunbgrlem3  48739  pgnbgreunbgrlem6  48745  pgn4cyclex  48747  isupwlkg  48758  rngcinvALTV  48897  ringcinvALTV  48931  srhmsubcALTV  48946  mapprop  48978  zlmodzxzadd  48990  domnmsuppn0  49001  ply1mulgsumlem2  49019  lincsum  49061  lincsumcl  49063  lincscmcl  49064  isldepslvec2  49117  digexp  49239  rrx2pnecoorneor  49347  rrx2pnedifcoorneorr  49349  rrx2xpref1o  49350  ehl2eudis0lt  49358  rrx2linest  49374  line2x  49386  itsclc0yqsollem2  49395  seppsepf  49559  thincn0eu  50061