Theorem anim12ci 589

Description: Variant of anim12i 588 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
anim12i.1	⊢ (𝜑 → 𝜓)
anim12i.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
anim12ci	⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Proof of Theorem anim12ci

Step	Hyp	Ref	Expression
1		anim12i.2	. . 3 ⊢ (𝜒 → 𝜃)
2		anim12i.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	anim12i 588	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜃 ∧ 𝜓))
4	3	ancoms 468	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  2exeu  2537  ideqg  5195  dfco2a  5552  frnssb  6298  fliftval  6466  omlimcl  7545  funsnfsupp  8182  ltrnq  9680  ltsrpr  9777  difelfznle  12322  nelfzo  12344  muladdmodid  12572  modmulmodr  12598  modsumfzodifsn  12605  hash2prd  13114  swrdccatin12lem2a  13336  repswswrd  13382  cshwidxm  13405  s3iunsndisj  13555  lcmftp  15187  ncoprmlnprm  15274  modprm0  15348  difsqpwdvds  15429  brssc  16297  resmhm  17182  mhmco  17185  gasubg  17558  idrespermg  17654  rhmco  18560  resrhm  18632  cply1mul  19485  dmatmul  20122  scmatf1  20156  slesolinv  20305  slesolinvbi  20306  slesolex  20307  cramerimplem3  20310  cramerimp  20311  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  bwth  21023  nmhmco  22370  chpchtsum  24744  gausslemma2dlem1a  24890  2lgslem1a1  24914  dchrisum0lem1  25005  wlkdvspthlem  26137  clwlkisclwwlklem0  26316  clwwlkf1  26324  wwlksubclwwlk  26332  clwlkfclwwlk  26371  clwlkf1clwwlklem  26376  vdgrf  26425  frgra3v  26529  frgrancvvdeqlem3  26559  frghash2spot  26590  numclwwlk3  26636  numclwwlk5  26639  frgrareg  26644  ex-ceil  26697  occon2  27531  bnj1110  30304  relowlssretop  32387  poimirlem16  32595  poimirlem19  32598  poimirlem30  32609  itgspltprt  38871  2rexreu  39834  iccpartiltu  39960  iccpartgt  39965  goldbachthlem1  39995  goldbachthlem2  39996  nn0e  40146  stgoldbwt  40198  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  subusgr  40513  isuvtxa  40621  iscplgredg  40639  crctcsh1wlkn0  41024  crctcsh  41027  rusgrnumwwlk  41178  clwlkclwwlklem3  41210  clwwlksf1  41224  clwlksfclwwlk  41269  clwlksf1clwwlklem  41275  eucrctshift  41411  frgr3v  41445  frgrncvvdeqlem3  41471  av-numclwwlk3  41539  av-frgrareg  41548  resmgmhm  41588  mgmhmco  41591  rnghmco  41697  ztprmneprm  41918  nn0sumltlt  41921  ldepspr  42056  m1modmmod  42110  blennngt2o2  42184  aacllem  42356