Theorem anim12ci 607

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anim1ci  609  2exeu  2729  ideqg  5506  dfco2a  5876  frnssb  6640  fliftval  6821  omlimcl  7925  funsnfsupp  8568  ltrnq  10116  ltsrpr  10214  difelfznle  12748  nelfzo  12770  muladdmodid  13005  modmulmodr  13031  modsumfzodifsn  13038  swrdnd0  13722  swrdccatin12lem2a  13823  repswswrd  13900  cshwidxm  13929  s3iunsndisj  14086  lcmftp  15722  ncoprmlnprm  15807  modprm0  15881  difsqpwdvds  15962  brssc  16826  resmhm  17712  mhmco  17715  gasubg  18085  idrespermg  18181  rhmco  19093  resrhm  19165  cply1mul  20024  dmatmul  20671  scmatf1  20705  slesolinv  20855  slesolinvbi  20856  slesolex  20857  cramerimplem3  20861  cramerimp  20862  chfacfscmulgsum  21035  chfacfpmmulgsum  21039  bwth  21584  nmhmco  22930  chpchtsum  25357  gausslemma2dlem1a  25503  2lgslem1a1  25527  dchrisum0lem1  25618  subusgr  26586  isuvtx  26693  iscplgredg  26715  structtocusgr  26744  crctcshwlkn0  27120  crctcsh  27123  rusgrnumwwlk  27305  clwlkclwwlklem3  27330  clwwlkf1OLD  27388  clwwlkf1  27393  clwlksfclwwlkOLD  27431  clwlksf1clwwlklemOLD  27437  eucrctshift  27609  frgr3v  27645  frgrwopreglem5a  27681  numclwwlk3  27789  frgrreg  27798  ex-ceil  27852  occon2  28691  bnj1110  31585  relowlssretop  33749  poimirlem16  33962  poimirlem19  33965  poimirlem30  33976  itgspltprt  40982  2rexreu  42003  iccpartiltu  42239  iccpartgt  42244  goldbachthlem1  42280  goldbachthlem2  42281  nn0e  42431  stgoldbwt  42487  bgoldbtbndlem3  42518  bgoldbtbndlem4  42519  bgoldbtbnd  42520  isomushgr  42537  isomuspgrlem1  42538  resmgmhm  42638  mgmhmco  42641  rnghmco  42747  ztprmneprm  42965  nn0sumltlt  42968  ldepspr  43102  m1modmmod  43156  blennngt2o2  43226  line2xlem  43298  aacllem  43436