Theorem anim12ci 615

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anim1ci  617  2exeuv  2713  2exeu  2727  2rexreu  3753  ideqg  5717  dfco2a  6094  frnssb  6880  fliftval  7063  omlimcl  8198  funsnfsupp  8851  ltrnq  10395  ltsrpr  10493  difelfznle  13015  nelfzo  13037  muladdmodid  13273  modmulmodr  13299  modsumfzodifsn  13306  ccatsymb  13930  swrdnd0  14013  pfxsuffeqwrdeq  14054  pfxccatin12lem2a  14083  repswswrd  14140  cshwidxm  14164  s3iunsndisj  14322  lcmftp  15974  ncoprmlnprm  16062  modprm0  16136  dvdsprmpweqle  16216  difsqpwdvds  16217  brssc  17078  resmhm  17979  mhmco  17982  idresefmnd  18058  gasubg  18426  idrespermg  18533  rhmco  19483  resrhm  19558  cply1mul  20456  dmatmul  21100  scmatf1  21134  slesolinv  21283  slesolinvbi  21284  slesolex  21285  cramerimplem3  21288  cramerimp  21289  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  bwth  22012  nmhmco  23359  chpchtsum  25789  gausslemma2dlem1a  25935  2lgslem1a1  25959  2sq2  26003  dchrisum0lem1  26086  subusgr  27065  isuvtx  27171  iscplgredg  27193  structtocusgr  27222  crctcshwlkn0  27593  crctcsh  27596  rusgrnumwwlk  27748  clwlkclwwlklem3  27773  clwwlkf1  27822  eucrctshift  28016  frgr3v  28048  frgrwopreglem5a  28084  numclwwlk3  28158  frgrreg  28167  ex-ceil  28221  occon2  29059  bnj1110  32249  satfv1lem  32604  relowlssretop  34638  poimirlem16  34902  poimirlem19  34905  poimirlem30  34916  pr2cv  39900  itgspltprt  42256  or2expropbilem1  43260  iccpartiltu  43575  iccpartgt  43580  ich2exprop  43626  goldbachthlem1  43700  goldbachthlem2  43701  nn0e  43855  nneven  43856  stgoldbwt  43934  bgoldbtbndlem3  43965  bgoldbtbndlem4  43966  bgoldbtbnd  43967  isomushgr  43984  isomuspgrlem1  43985  resmgmhm  44058  mgmhmco  44061  rnghmco  44171  ztprmneprm  44388  nn0sumltlt  44391  ldepspr  44521  m1modmmod  44574  blennngt2o2  44645  line2xlem  44733  aacllem  44895