Theorem anim12ci 623

Description: Variant of anim12i 622 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 622	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜃 ∧ 𝜓))
4	3	ancoms 462	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anim1ci  625  2exeuv  2658  2exeu  2672  2rexreu  3724  ideqg  5821  dfco2a  6229  fcdmssb  7099  fliftval  7296  ord1eln01  8460  omlimcl  8542  brinxper  8703  ssfi  9137  funsnfsupp  9335  ltrnq  10934  ltsrpr  11032  difelfznle  13644  nelfzo  13667  modaddid  13917  muladdmodid  13920  modmulmodr  13947  modsumfzodifsn  13954  ccatsymb  14593  swrdnd0  14668  pfxsuffeqwrdeq  14708  pfxccatin12lem2a  14737  repswswrd  14794  cshwidxm  14818  s3iunsndisj  14978  lcmftp  16653  ncoprmlnprm  16746  modprm0  16824  dvdsprmpweqle  16905  difsqpwdvds  16906  brssc  17830  resmgmhm  18728  mgmhmco  18731  resmhm  18837  mhmco  18840  idresefmnd  18916  gasubg  19325  idrespermg  19434  rnghmco  20485  rhmco  20529  resrhm  20630  cply1mul  22339  dmatmul  22537  scmatf1  22571  slesolinv  22720  slesolinvbi  22721  slesolex  22722  cramerimplem3  22725  cramerimp  22726  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  bwth  23450  nmhmco  24796  chpchtsum  27260  gausslemma2dlem1a  27406  2lgslem1a1  27430  2sq2  27474  dchrisum0lem1  27557  subusgr  29436  isuvtx  29542  iscplgredg  29564  structtocusgr  29593  crctcshwlkn0  29967  crctcsh  29970  rusgrnumwwlk  30124  clwlkclwwlklem3  30149  clwwlkf1  30197  eucrctshift  30391  frgr3v  30423  frgrwopreglem5a  30459  numclwwlk3  30533  frgrreg  30542  ex-ceil  30596  occon2  31437  bnj1110  35241  satfv1lem  35676  relowlssretop  37821  poimirlem16  38099  poimirlem19  38102  poimirlem30  38113  omlimcl2  43783  pr2cv  44088  itgspltprt  46517  or2expropbilem1  47590  addmodne  47908  m1modmmod  47922  mod2addne  47928  iccpartiltu  47992  iccpartgt  47997  ich2exprop  48041  nprmmul2  48098  goldbachthlem1  48118  goldbachthlem2  48119  nn0e  48283  nneven  48284  stgoldbwt  48362  bgoldbtbndlem3  48393  bgoldbtbndlem4  48394  bgoldbtbnd  48395  isubgruhgr  48454  gricushgr  48503  isubgr3stgrlem7  48558  gpgedgvtx1  48648  ztprmneprm  48933  nn0sumltlt  48936  ldepspr  49059  blennngt2o2  49178  line2xlem  49339  aacllem  50386