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 459	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anim1ci  616  2exeuv  2628  2exeu  2642  2rexreu  3758  ideqg  5851  dfco2a  6245  fcdmssb  7123  fliftval  7315  ord1eln01  8498  omlimcl  8580  ssfi  9175  funsnfsupp  9389  ltrnq  10976  ltsrpr  11074  difelfznle  13617  nelfzo  13639  muladdmodid  13878  modmulmodr  13904  modsumfzodifsn  13911  ccatsymb  14534  swrdnd0  14609  pfxsuffeqwrdeq  14650  pfxccatin12lem2a  14679  repswswrd  14736  cshwidxm  14760  s3iunsndisj  14917  lcmftp  16575  ncoprmlnprm  16666  modprm0  16740  dvdsprmpweqle  16821  difsqpwdvds  16822  brssc  17763  resmhm  18703  mhmco  18706  idresefmnd  18782  gasubg  19168  idrespermg  19281  rhmco  20280  resrhm  20352  cply1mul  21825  dmatmul  22006  scmatf1  22040  slesolinv  22189  slesolinvbi  22190  slesolex  22191  cramerimplem3  22194  cramerimp  22195  chfacfscmulgsum  22369  chfacfpmmulgsum  22373  bwth  22921  nmhmco  24280  chpchtsum  26729  gausslemma2dlem1a  26875  2lgslem1a1  26899  2sq2  26943  dchrisum0lem1  27026  subusgr  28584  isuvtx  28690  iscplgredg  28712  structtocusgr  28741  crctcshwlkn0  29113  crctcsh  29116  rusgrnumwwlk  29267  clwlkclwwlklem3  29292  clwwlkf1  29340  eucrctshift  29534  frgr3v  29566  frgrwopreglem5a  29602  numclwwlk3  29676  frgrreg  29685  ex-ceil  29739  occon2  30579  bnj1110  34062  satfv1lem  34422  relowlssretop  36330  poimirlem16  36590  poimirlem19  36593  poimirlem30  36604  omlimcl2  42073  pr2cv  42381  itgspltprt  44774  or2expropbilem1  45821  iccpartiltu  46169  iccpartgt  46174  ich2exprop  46218  goldbachthlem1  46292  goldbachthlem2  46293  nn0e  46444  nneven  46445  stgoldbwt  46523  bgoldbtbndlem3  46554  bgoldbtbndlem4  46555  bgoldbtbnd  46556  isomushgr  46573  isomuspgrlem1  46574  resmgmhm  46647  mgmhmco  46650  rnghmco  46785  ztprmneprm  47102  nn0sumltlt  47105  ldepspr  47232  m1modmmod  47285  blennngt2o2  47356  line2xlem  47517  aacllem  47926