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  2717  2exeu  2731  2rexreu  3753  ideqg  5722  dfco2a  6099  frnssb  6885  fliftval  7069  omlimcl  8204  funsnfsupp  8857  ltrnq  10401  ltsrpr  10499  difelfznle  13022  nelfzo  13044  muladdmodid  13280  modmulmodr  13306  modsumfzodifsn  13313  ccatsymb  13936  swrdnd0  14019  pfxsuffeqwrdeq  14060  pfxccatin12lem2a  14089  repswswrd  14146  cshwidxm  14170  s3iunsndisj  14328  lcmftp  15980  ncoprmlnprm  16068  modprm0  16142  dvdsprmpweqle  16222  difsqpwdvds  16223  brssc  17084  resmhm  17985  mhmco  17988  idresefmnd  18064  gasubg  18432  idrespermg  18539  rhmco  19489  resrhm  19564  cply1mul  20462  dmatmul  21106  scmatf1  21140  slesolinv  21289  slesolinvbi  21290  slesolex  21291  cramerimplem3  21294  cramerimp  21295  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  bwth  22018  nmhmco  23365  chpchtsum  25795  gausslemma2dlem1a  25941  2lgslem1a1  25965  2sq2  26009  dchrisum0lem1  26092  subusgr  27071  isuvtx  27177  iscplgredg  27199  structtocusgr  27228  crctcshwlkn0  27599  crctcsh  27602  rusgrnumwwlk  27754  clwlkclwwlklem3  27779  clwwlkf1  27828  eucrctshift  28022  frgr3v  28054  frgrwopreglem5a  28090  numclwwlk3  28164  frgrreg  28173  ex-ceil  28227  occon2  29065  bnj1110  32254  satfv1lem  32609  relowlssretop  34647  poimirlem16  34923  poimirlem19  34926  poimirlem30  34937  pr2cv  39956  itgspltprt  42313  or2expropbilem1  43316  iccpartiltu  43631  iccpartgt  43636  ich2exprop  43682  goldbachthlem1  43756  goldbachthlem2  43757  nn0e  43911  nneven  43912  stgoldbwt  43990  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomushgr  44040  isomuspgrlem1  44041  resmgmhm  44114  mgmhmco  44117  rnghmco  44227  ztprmneprm  44444  nn0sumltlt  44447  ldepspr  44577  m1modmmod  44630  blennngt2o2  44701  line2xlem  44789  aacllem  44951