Theorem anim12i 625

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12ci  626  anim1i  627  anim2i  629  anifp  1088  cgsex2g  3496  cgsex4g  3497  spc2egv  3554  spc2ed  3556  uneqin  4235  2reu4lem  4479  2reu4  4480  disjpr2  4674  ssunieq  4904  iuneq1  4968  iuneq2  4971  copsex2t  5464  propeqop  5479  opthhausdorff  5490  opthhausdorff0  5491  iunopeqop  5494  iunopeqopOLD  5495  soeq2  5581  opbrop  5749  xpsspw  5787  coeq1  5835  coeq2  5836  cnveq  5851  dmeq  5885  sotri  6121  tz7.7  6387  funun  6584  fununfun  6586  fundif  6587  funprg  6592  funtp  6595  2elresin  6658  funssxp  6736  fssres  6746  f1cof1  6788  foun  6841  f1un  6843  resdif  6844  f1oco  6846  fvun  6973  elfvmptrab1w  7019  elfvmptrab1  7020  fvn0ssdmfun  7072  dff3  7098  exfo  7103  fprg  7157  ftpg  7158  f1ounsn  7278  weisoeq2  7364  oprabv  7478  ndmovdistr  7608  ndmovord  7609  brrpssg  7739  eldifpw  7780  iunpw  7783  epweon  7787  bropfvvvv  8101  f1o2ndf1  8131  poseq  8168  fvn0elsupp  8190  smores  8353  tz7.49  8448  tz7.49c  8449  oaord  8548  oeeulem  8603  nnaord  8621  brecop  8824  brecop2  8825  eroveu  8826  ecopovtrn  8834  ixpeq2  8932  undifixp  8955  sbthlem8  9106  sbthlem9  9107  unxpdom  9243  isinf  9249  f1opwfi  9338  fiin  9407  en2lp  9600  inf3lem3  9624  brttrcl  9707  tcmin  9733  djuexb  9983  alephfp  10180  kmlem16  10237  endjudisj  10240  cofsmo  10340  fin23lem28  10411  axdc3lem2  10522  ac6c4  10552  brdom3  10600  brdom5  10601  brdom4  10602  canthp1lem2  10731  finngch  10733  ordpipq  11020  adderpq  11034  mulerpq  11035  lterpq  11048  genpn0  11081  genpnnp  11083  addclprlem2  11095  addcmpblnr  11147  addsrpr  11153  mulsrpr  11154  addclsr  11161  addasssr  11166  distrsr  11169  0idsr  11175  1idsr  11176  00sr  11177  mulgt0sr  11183  axaddf  11223  axaddass  11234  axdistr  11236  cnegex  11484  recextlem2  11940  difgtsumgt  12652  zaddcl  12729  qaddcl  13086  qmulcl  13088  qreccl  13090  xmulgt0  13406  xrsupsslem  13430  xrinfmsslem  13431  supxrpnf  13441  iccss  13538  difreicc  13608  fzadd2  13686  fzsubel  13687  ssfzunsnext  13696  difelfznle  13769  2ffzeq  13776  nelfzo  13792  fzonmapblen  13836  ubmelfzo  13858  ubmelm1fzo  13891  elfznelfzo  13901  subfzo0  13921  adddivflid  13951  modaddid  14043  modifeq2int  14069  modaddmodup  14070  addmodlteq  14082  fsuppmapnn0fiub  14127  mulexp  14237  mulexpz  14238  leexp1a  14311  faclbnd  14427  hashunx  14523  hashgt23el  14562  wrdeq  14674  ccatcl  14712  swrdnd  14797  swrdnd0  14800  swrdsbslen  14807  swrdspsleq  14808  pfxccat1  14844  swrdswrdlem  14846  pfxccatin12lem2a  14869  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccatin12  14875  swrdccat  14877  reuccatpfxs1  14889  repswswrd  14928  repswccat  14930  cshwidxn  14953  cshweqdif2  14963  2cshwcshw  14969  cshwcshid  14971  cshwcsh2id  14972  f1oun2prg  15061  s2eq2s1eq  15080  s3eqs2s1eq  15082  s3sndisj  15113  s3iunsndisj  15114  sqabsadd  15442  sqabssub  15443  abs2dif  15493  rexanuz  15506  o1of2  15773  o1rlimmul  15779  fsum2dlem  15929  isumltss  16010  fprodser  16109  fprodeq0  16135  fprod2dlem  16140  dvdscmulr  16447  dvdsmulcr  16448  summodnegmod  16449  difmod0  16450  dvds2ln  16452  dvdsflip  16480  divalglem9  16564  gcdcllem3  16664  gcdaddmlem  16689  sqgcd  16729  lcmcllem  16764  lcmabs  16773  lcmgcdlem  16774  lcmgcd  16775  lcmgcdeq  16780  lcmftp  16804  lcmfunsnlem2lem1  16806  qredeq  16825  cncongr1  16835  cncongr2  16836  isprm7  16877  hashgcdlem  16958  dvdsprmpweqle  17057  difsqpwdvds  17058  prmgaplem4  17225  cshwsidrepsw  17264  setsfun0  17343  setsstruct2  17345  xpsfrnel2  17729  isfunc  18032  tsrss  18756  chnpof1  18797  rabsubmgmd  18886  resmgmhm2  18894  mndpfsupp  18954  ismhm0  18978  mhmismgmhm  18979  mndissubm  18995  resmndismnd  18996  resmhm2  19010  submefmnd  19084  sursubmefmnd  19085  injsubmefmnd  19086  grpissubg  19350  gimco  19475  symg2bas  19600  pgrpsubgsymg  19616  symgextf  19624  fvcosymgeq  19636  gsmsymgreqlem1  19637  symgfixf1  19644  efgrelexlema  19956  gsum2dlem1  20177  gsum2dlem2  20178  dvdsr  20585  isrnghmmul  20665  c0ghm  20684  rhmisrnghm  20704  rimco  20740  subrngpropd  20813  subrgpropd  20853  rnghmsubcsetclem2  20877  rngcinv  20882  rhmsubcsetclem2  20906  rhmsubcrngclem2  20912  ringcinv  20916  srhmsubc  20925  isdrng3lem2  20999  islmhm2  21306  unichnlidl  21509  cmprmidlmcl  21624  psgnghm  21879  psgndiflemB  21899  frlmbas3  22075  frlmphl  22080  islindf4  22137  ressmpladd  22330  ressmplmul  22331  mplind  22372  mpomatmul  22754  mavmul0g  22861  1marepvsma1  22891  mdetdiag  22907  matunitlindflem1  22987  matunitlindflem2  22988  slesolvec  22990  cramerimplem2  22995  cramerimplem3  22996  cramerimp  22997  mat2pmatlin  23046  m2pmfzgsumcl  23059  monmatcollpw  23090  pmatcollpw3lem  23094  pmatcollpwscmatlem1  23100  chpmat1dlem  23146  chfacfisf  23165  chfacfisfcpmat  23166  chfacfpmmulgsum2  23176  tgcl  23280  uncld  23352  innei  23436  cnco  23577  uncmp  23714  txbas  23879  txbasval  23918  tx1stc  23962  fbun  24152  infil  24175  fbunfip  24181  filuni  24197  imaelfm  24263  txflf  24318  tsmsfbas  24440  tsmsxp  24467  blin2  24741  nmhmplusg  25069  qtopbaslem  25070  iccntr  25134  ncvspi  25470  ncvs1  25471  unmbl  25851  volfiniun  25861  mbfi1flimlem  26036  ply1idom  26436  logreclem  27083  relogbcxpb  27108  fsumvma2  27534  chpchtsum  27539  dchrelbas3  27558  dchrmulcl  27569  lgsmulsqcoprm  27663  gausslemma2dlem1a  27685  lgsquad2lem2  27705  dchrisum0fmul  27826  dchrisum0lem1  27836  ltsres  28012  nocvxminlem  28133  oldlim  28266  madebdayim  28267  madebdaylemlrcut  28278  readdscl  28878  remulscl  28881  ishpg  29230  brcgr  29471  brbtwn2  29476  axcontlem2  29536  uspgredg2v  29798  usgredg2v  29801  usgr2v1e2w  29826  nb3gr2nb  29958  cusgredg  29998  cplgr3v  30009  cusgrop  30012  rusgr1vtx  30162  iswlkg  30187  wlkeq  30207  wlk1walk  30212  uspgr2wlkeq2  30220  uspgr2wlkeqi  30221  cyclnumvtx  30381  crctcshwlkn0lem3  30394  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  wspthneq1eq2  30442  wwlksnextinj  30481  2wlkdlem7  30514  2wlkdlem8  30515  2pthon3v  30525  s3wwlks2on  30538  sps3wwlks2on  30539  elwwlks2  30551  elwspths2spth  30552  rusgrnumwwlks  30559  clwlkclwwlklem2a  30582  clwlkclwwlklem3  30585  clwlkclwwlkf1lem2  30589  clwlkclwwlkf1  30594  clwwlknonex2  30693  3wlkdlem3  30755  uhgr3cyclex  30776  cusconngr  30785  eupth0  30808  frgr3v  30869  1to3vfriswmgr  30874  4cycl2v2nb  30883  frgrnbnb  30887  frgrncvvdeq  30903  frgrwopreglem4a  30904  frgrwopreglem5a  30905  frgrwopreglem4  30909  frgrwopreglem5  30915  frgrhash2wsp  30926  numclwwlk1lem2foa  30948  numclwwlk2  30975  blocni  31400  hvsub4  31632  shscli  31912  shscom  31914  spanunsni  32174  spanpr  32175  5oalem2  32250  5oalem3  32251  5oalem5  32253  3oalem1  32257  hoscl  32340  hoadddi  32398  hoadddir  32399  hosub4  32408  lnophsi  32596  hmops  32615  hmopm  32616  adjadd  32688  leop2  32719  leopadd  32727  leopmuli  32728  pjclem4  32794  pj3si  32802  mdslmd1lem2  32921  mdslmd3i  32927  atomli  32977  atcvatlem  32980  chirredlem3  32987  chirredi  32989  atcvat3i  32991  mdsymlem1  32998  mdsymlem5  33002  cdjreui  33027  cdj3i  33036  addltmulALT  33041  hashxpe  33392  domnmuln0rd  33831  mndpluscn  34551  sxbrsigalem5  34913  probfinmeasbALTV  35054  bnj545  35518  bnj546  35519  bnj557  35524  bnj570  35528  bnj594  35535  bnj1001  35582  bnj1118  35607  txpconn  35976  cvmlift2lem10  36056  gonar  36139  lediv2aALT  36421  altopeq12  36707  altxpsspw  36722  funtransport  36776  neibastop1  37127  filnetlem3  37148  lukshef-ax2  37183  arg-ax  37184  nndivsub  37225  bj-nnfan  37636  bj-nnfor  37638  cgsex2gd  38038  copsex2b  38041  isbasisrelowllem1  38258  isbasisrelowllem2  38259  icoreclin  38260  relowlssretop  38266  rdgeqoa  38273  fvineqsnf1  38313  poimirlem4  38522  poimirlem26  38544  poimirlem29  38547  poimirlem30  38548  heicant  38553  mblfinlem1  38555  ismblfin  38559  itg2addnclem  38569  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  impprop  38624  prdstotbnd  38708  heibor1lem  38723  isdrngo2  38872  divrngidl  38942  pridlc3  38987  eldisjdmqsim  39729  linepsubN  40789  pmapsub  40805  elpaddri  40839  paddasslem14  40870  pmapjoin  40889  dvhfvadd  42128  dvhvaddcomN  42133  bcle2d  43209  imacrhmcl  43561  rmxynorm  43904  monotoddzzfi  43928  acongtr  43964  mpaaeu  44136  oaltublim  44276  omord2lim  44286  cantnftermord  44306  dflim5  44315  omabs2  44318  tfsconcat0i  44331  ofoafo  44342  naddcnff  44348  oaun3lem1  44360  oaun3lem2  44361  pr2cv  44533  brfvrcld2  44677  rfovcnvf1od  44989  ismnushort  45270  nzin  45287  pm10.14  45328  disjrnmpt2  46172  liminfvalxr  46762  etransclem38  47251  wrddin  47865  cfsetsnfsetf1  48098  tz6.12-afv2  48279  2elfz2melfz  48357  fz0addge0  48358  2ffzoeq  48367  difltmodne  48387  modn0mul  48402  mod2addne  48409  icceuelpartlem  48486  icceuelpart  48487  ich2exprop  48522  sqrtpwpw2p  48592  fmtnoprmfac1lem  48618  fmtnoprmfac1  48619  lighneallem2  48660  divgcdoddALTV  48749  gbowpos  48826  gbowgt5  48829  gboge9  48831  nnsum3primesgbe  48859  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  isuspgrim  48963  clnbgrgrimlem  49000  clnbgrgrim  49001  isgrtri  49010  isubgr3stgrlem4  49036  grlimgrtri  49070  grlictr  49082  gpgedgvtx0  49128  gpgedg2iv  49134  gpg5nbgrvtx03star  49147  gpg5nbgr3star  49148  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  pgn4cyclex  49193  isupwlkg  49204  rngcinvALTV  49342  ringcinvALTV  49376  srhmsubcALTV  49391  mapprop  49427  zlmodzxzadd  49439  domnmsuppn0  49450  ply1mulgsumlem2  49468  lincsum  49510  lincsumcl  49512  lincscmcl  49513  isldepslvec2  49566  digexp  49688  rrx2pnecoorneor  49796  rrx2pnedifcoorneorr  49798  rrx2xpref1o  49799  ehl2eudis0lt  49807  rrx2linest  49823  line2x  49835  itsclc0yqsollem2  49844  seppsepf  50006  thincn0eu  50508  alseu-no-surprise  50903