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  2629  2exeu  2643  2rexreu  3717  ideqg  5797  dfco2a  6200  fcdmssb  7063  fliftval  7258  ord1eln01  8419  omlimcl  8501  brinxper  8659  ssfi  9091  funsnfsupp  9285  ltrnq  10879  ltsrpr  10977  difelfznle  13546  nelfzo  13568  modaddid  13818  muladdmodid  13821  modmulmodr  13848  modsumfzodifsn  13855  ccatsymb  14494  swrdnd0  14569  pfxsuffeqwrdeq  14609  pfxccatin12lem2a  14638  repswswrd  14695  cshwidxm  14719  s3iunsndisj  14879  lcmftp  16551  ncoprmlnprm  16643  modprm0  16721  dvdsprmpweqle  16802  difsqpwdvds  16803  brssc  17725  resmgmhm  18623  mgmhmco  18626  resmhm  18732  mhmco  18735  idresefmnd  18811  gasubg  19218  idrespermg  19327  rnghmco  20379  rhmco  20420  resrhm  20520  cply1mul  22214  dmatmul  22415  scmatf1  22449  slesolinv  22598  slesolinvbi  22599  slesolex  22600  cramerimplem3  22603  cramerimp  22604  chfacfscmulgsum  22778  chfacfpmmulgsum  22782  bwth  23328  nmhmco  24674  chpchtsum  27160  gausslemma2dlem1a  27306  2lgslem1a1  27330  2sq2  27374  dchrisum0lem1  27457  subusgr  29271  isuvtx  29377  iscplgredg  29399  structtocusgr  29428  crctcshwlkn0  29803  crctcsh  29806  rusgrnumwwlk  29960  clwlkclwwlklem3  29985  clwwlkf1  30033  eucrctshift  30227  frgr3v  30259  frgrwopreglem5a  30295  numclwwlk3  30369  frgrreg  30378  ex-ceil  30432  occon2  31272  bnj1110  35017  satfv1lem  35429  relowlssretop  37430  poimirlem16  37699  poimirlem19  37702  poimirlem30  37713  omlimcl2  43362  pr2cv  43668  itgspltprt  46104  or2expropbilem1  47159  addmodne  47471  m1modmmod  47485  mod2addne  47491  iccpartiltu  47549  iccpartgt  47554  ich2exprop  47598  goldbachthlem1  47672  goldbachthlem2  47673  nn0e  47824  nneven  47825  stgoldbwt  47903  bgoldbtbndlem3  47934  bgoldbtbndlem4  47935  bgoldbtbnd  47936  isubgruhgr  47995  gricushgr  48044  isubgr3stgrlem7  48099  gpgedgvtx1  48189  ztprmneprm  48474  nn0sumltlt  48477  ldepspr  48601  blennngt2o2  48720  line2xlem  48881  aacllem  49929