Theorem anim12ci 617

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anim1ci  619  2exeuv  2635  2exeu  2649  2rexreu  3661  ideqg  5694  dfco2a  6079  frnssb  6895  fliftval  7082  omlimcl  8235  ssfi  8772  funsnfsupp  8930  ltrnq  10479  ltsrpr  10577  difelfznle  13112  nelfzo  13134  muladdmodid  13370  modmulmodr  13396  modsumfzodifsn  13403  ccatsymb  14025  swrdnd0  14108  pfxsuffeqwrdeq  14149  pfxccatin12lem2a  14178  repswswrd  14235  cshwidxm  14259  s3iunsndisj  14417  lcmftp  16077  ncoprmlnprm  16168  modprm0  16242  dvdsprmpweqle  16322  difsqpwdvds  16323  brssc  17189  resmhm  18101  mhmco  18104  idresefmnd  18180  gasubg  18550  idrespermg  18657  rhmco  19611  resrhm  19683  cply1mul  21069  dmatmul  21248  scmatf1  21282  slesolinv  21431  slesolinvbi  21432  slesolex  21433  cramerimplem3  21436  cramerimp  21437  chfacfscmulgsum  21611  chfacfpmmulgsum  21615  bwth  22161  nmhmco  23509  chpchtsum  25955  gausslemma2dlem1a  26101  2lgslem1a1  26125  2sq2  26169  dchrisum0lem1  26252  subusgr  27231  isuvtx  27337  iscplgredg  27359  structtocusgr  27388  crctcshwlkn0  27759  crctcsh  27762  rusgrnumwwlk  27913  clwlkclwwlklem3  27938  clwwlkf1  27986  eucrctshift  28180  frgr3v  28212  frgrwopreglem5a  28248  numclwwlk3  28322  frgrreg  28331  ex-ceil  28385  occon2  29223  bnj1110  32533  satfv1lem  32895  relowlssretop  35157  poimirlem16  35416  poimirlem19  35419  poimirlem30  35430  pr2cv  40700  itgspltprt  43062  or2expropbilem1  44065  iccpartiltu  44408  iccpartgt  44413  ich2exprop  44457  goldbachthlem1  44531  goldbachthlem2  44532  nn0e  44683  nneven  44684  stgoldbwt  44762  bgoldbtbndlem3  44793  bgoldbtbndlem4  44794  bgoldbtbnd  44795  isomushgr  44812  isomuspgrlem1  44813  resmgmhm  44886  mgmhmco  44889  rnghmco  44999  ztprmneprm  45217  nn0sumltlt  45220  ldepspr  45348  m1modmmod  45401  blennngt2o2  45472  line2xlem  45633  aacllem  45958