Theorem anim12ci 615

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anim1ci  617  2exeuv  2632  2exeu  2646  2rexreu  3708  ideqg  5806  dfco2a  6210  fcdmssb  7074  fliftval  7271  ord1eln01  8431  omlimcl  8513  brinxper  8673  ssfi  9107  funsnfsupp  9305  ltrnq  10902  ltsrpr  11000  difelfznle  13596  nelfzo  13619  modaddid  13869  muladdmodid  13872  modmulmodr  13899  modsumfzodifsn  13906  ccatsymb  14545  swrdnd0  14620  pfxsuffeqwrdeq  14660  pfxccatin12lem2a  14689  repswswrd  14746  cshwidxm  14770  s3iunsndisj  14930  lcmftp  16605  ncoprmlnprm  16698  modprm0  16776  dvdsprmpweqle  16857  difsqpwdvds  16858  brssc  17781  resmgmhm  18679  mgmhmco  18682  resmhm  18788  mhmco  18791  idresefmnd  18867  gasubg  19277  idrespermg  19386  rnghmco  20437  rhmco  20478  resrhm  20578  cply1mul  22261  dmatmul  22462  scmatf1  22496  slesolinv  22645  slesolinvbi  22646  slesolex  22647  cramerimplem3  22650  cramerimp  22651  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  bwth  23375  nmhmco  24721  chpchtsum  27182  gausslemma2dlem1a  27328  2lgslem1a1  27352  2sq2  27396  dchrisum0lem1  27479  subusgr  29358  isuvtx  29464  iscplgredg  29486  structtocusgr  29515  crctcshwlkn0  29889  crctcsh  29892  rusgrnumwwlk  30046  clwlkclwwlklem3  30071  clwwlkf1  30119  eucrctshift  30313  frgr3v  30345  frgrwopreglem5a  30381  numclwwlk3  30455  frgrreg  30464  ex-ceil  30518  occon2  31359  bnj1110  35124  satfv1lem  35544  relowlssretop  37679  poimirlem16  37957  poimirlem19  37960  poimirlem30  37971  omlimcl2  43670  pr2cv  43975  itgspltprt  46407  or2expropbilem1  47480  addmodne  47798  m1modmmod  47812  mod2addne  47818  iccpartiltu  47882  iccpartgt  47887  ich2exprop  47931  nprmmul2  47988  goldbachthlem1  48008  goldbachthlem2  48009  nn0e  48173  nneven  48174  stgoldbwt  48252  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  isubgruhgr  48344  gricushgr  48393  isubgr3stgrlem7  48448  gpgedgvtx1  48538  ztprmneprm  48823  nn0sumltlt  48826  ldepspr  48949  blennngt2o2  49068  line2xlem  49229  aacllem  50276