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  2632  2exeu  2646  2rexreu  3720  ideqg  5800  dfco2a  6204  fcdmssb  7067  fliftval  7262  ord1eln01  8423  omlimcl  8505  brinxper  8664  ssfi  9097  funsnfsupp  9295  ltrnq  10890  ltsrpr  10988  difelfznle  13558  nelfzo  13580  modaddid  13830  muladdmodid  13833  modmulmodr  13860  modsumfzodifsn  13867  ccatsymb  14506  swrdnd0  14581  pfxsuffeqwrdeq  14621  pfxccatin12lem2a  14650  repswswrd  14707  cshwidxm  14731  s3iunsndisj  14891  lcmftp  16563  ncoprmlnprm  16655  modprm0  16733  dvdsprmpweqle  16814  difsqpwdvds  16815  brssc  17738  resmgmhm  18636  mgmhmco  18639  resmhm  18745  mhmco  18748  idresefmnd  18824  gasubg  19231  idrespermg  19340  rnghmco  20393  rhmco  20434  resrhm  20534  cply1mul  22240  dmatmul  22441  scmatf1  22475  slesolinv  22624  slesolinvbi  22625  slesolex  22626  cramerimplem3  22629  cramerimp  22630  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  bwth  23354  nmhmco  24700  chpchtsum  27186  gausslemma2dlem1a  27332  2lgslem1a1  27356  2sq2  27400  dchrisum0lem1  27483  subusgr  29362  isuvtx  29468  iscplgredg  29490  structtocusgr  29519  crctcshwlkn0  29894  crctcsh  29897  rusgrnumwwlk  30051  clwlkclwwlklem3  30076  clwwlkf1  30124  eucrctshift  30318  frgr3v  30350  frgrwopreglem5a  30386  numclwwlk3  30460  frgrreg  30469  ex-ceil  30523  occon2  31363  bnj1110  35138  satfv1lem  35556  relowlssretop  37568  poimirlem16  37837  poimirlem19  37840  poimirlem30  37851  omlimcl2  43484  pr2cv  43789  itgspltprt  46223  or2expropbilem1  47278  addmodne  47590  m1modmmod  47604  mod2addne  47610  iccpartiltu  47668  iccpartgt  47673  ich2exprop  47717  goldbachthlem1  47791  goldbachthlem2  47792  nn0e  47943  nneven  47944  stgoldbwt  48022  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  isubgruhgr  48114  gricushgr  48163  isubgr3stgrlem7  48218  gpgedgvtx1  48308  ztprmneprm  48593  nn0sumltlt  48596  ldepspr  48719  blennngt2o2  48838  line2xlem  48999  aacllem  50046