Theorem anim12ci 614

Description: Variant of anim12i 613 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 613	. 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  616  2exeuv  2632  2exeu  2646  2rexreu  3750  ideqg  5836  dfco2a  6240  fcdmssb  7117  fliftval  7314  ord1eln01  8513  omlimcl  8595  brinxper  8753  ssfi  9192  funsnfsupp  9409  ltrnq  10998  ltsrpr  11096  difelfznle  13664  nelfzo  13686  muladdmodid  13933  modmulmodr  13960  modsumfzodifsn  13967  ccatsymb  14605  swrdnd0  14680  pfxsuffeqwrdeq  14721  pfxccatin12lem2a  14750  repswswrd  14807  cshwidxm  14831  s3iunsndisj  14992  lcmftp  16660  ncoprmlnprm  16752  modprm0  16830  dvdsprmpweqle  16911  difsqpwdvds  16912  brssc  17832  resmgmhm  18694  mgmhmco  18697  resmhm  18803  mhmco  18806  idresefmnd  18882  gasubg  19290  idrespermg  19397  rnghmco  20422  rhmco  20466  resrhm  20566  cply1mul  22239  dmatmul  22440  scmatf1  22474  slesolinv  22623  slesolinvbi  22624  slesolex  22625  cramerimplem3  22628  cramerimp  22629  chfacfscmulgsum  22803  chfacfpmmulgsum  22807  bwth  23353  nmhmco  24700  chpchtsum  27187  gausslemma2dlem1a  27333  2lgslem1a1  27357  2sq2  27401  dchrisum0lem1  27484  subusgr  29273  isuvtx  29379  iscplgredg  29401  structtocusgr  29430  crctcshwlkn0  29808  crctcsh  29811  rusgrnumwwlk  29962  clwlkclwwlklem3  29987  clwwlkf1  30035  eucrctshift  30229  frgr3v  30261  frgrwopreglem5a  30297  numclwwlk3  30371  frgrreg  30380  ex-ceil  30434  occon2  31274  bnj1110  35018  satfv1lem  35389  relowlssretop  37386  poimirlem16  37665  poimirlem19  37668  poimirlem30  37679  omlimcl2  43241  pr2cv  43547  itgspltprt  45988  or2expropbilem1  47041  addmodne  47353  iccpartiltu  47416  iccpartgt  47421  ich2exprop  47465  goldbachthlem1  47539  goldbachthlem2  47540  nn0e  47691  nneven  47692  stgoldbwt  47770  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  isubgruhgr  47861  gricushgr  47910  isubgr3stgrlem7  47964  gpgedgvtx1  48046  ztprmneprm  48302  nn0sumltlt  48305  ldepspr  48429  m1modmmod  48481  blennngt2o2  48552  line2xlem  48713  aacllem  49645