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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anim1ci  616  2exeuv  2631  2exeu  2645  2rexreu  3767  ideqg  5861  dfco2a  6265  fcdmssb  7141  fliftval  7337  ord1eln01  8535  omlimcl  8617  brinxper  8775  ssfi  9214  funsnfsupp  9433  ltrnq  11020  ltsrpr  11118  difelfznle  13683  nelfzo  13705  muladdmodid  13952  modmulmodr  13979  modsumfzodifsn  13986  ccatsymb  14621  swrdnd0  14696  pfxsuffeqwrdeq  14737  pfxccatin12lem2a  14766  repswswrd  14823  cshwidxm  14847  s3iunsndisj  15008  lcmftp  16674  ncoprmlnprm  16766  modprm0  16844  dvdsprmpweqle  16925  difsqpwdvds  16926  brssc  17859  resmgmhm  18725  mgmhmco  18728  resmhm  18834  mhmco  18837  idresefmnd  18913  gasubg  19321  idrespermg  19430  rnghmco  20458  rhmco  20502  resrhm  20602  cply1mul  22301  dmatmul  22504  scmatf1  22538  slesolinv  22687  slesolinvbi  22688  slesolex  22689  cramerimplem3  22692  cramerimp  22693  chfacfscmulgsum  22867  chfacfpmmulgsum  22871  bwth  23419  nmhmco  24778  chpchtsum  27264  gausslemma2dlem1a  27410  2lgslem1a1  27434  2sq2  27478  dchrisum0lem1  27561  subusgr  29307  isuvtx  29413  iscplgredg  29435  structtocusgr  29464  crctcshwlkn0  29842  crctcsh  29845  rusgrnumwwlk  29996  clwlkclwwlklem3  30021  clwwlkf1  30069  eucrctshift  30263  frgr3v  30295  frgrwopreglem5a  30331  numclwwlk3  30405  frgrreg  30414  ex-ceil  30468  occon2  31308  bnj1110  34997  satfv1lem  35368  relowlssretop  37365  poimirlem16  37644  poimirlem19  37647  poimirlem30  37658  omlimcl2  43259  pr2cv  43566  itgspltprt  45999  or2expropbilem1  47049  addmodne  47351  iccpartiltu  47414  iccpartgt  47419  ich2exprop  47463  goldbachthlem1  47537  goldbachthlem2  47538  nn0e  47689  nneven  47690  stgoldbwt  47768  bgoldbtbndlem3  47799  bgoldbtbndlem4  47800  bgoldbtbnd  47801  isubgruhgr  47859  gricushgr  47891  isubgr3stgrlem7  47944  gpgedgvtx1  48025  ztprmneprm  48268  nn0sumltlt  48271  ldepspr  48395  m1modmmod  48447  blennngt2o2  48518  line2xlem  48679  aacllem  49375