Theorem anim12ci 626

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim1ci  628  2exeuv  2657  2exeu  2671  2rexreu  3719  ideqg  5828  dfco2a  6247  fcdmssb  7123  fliftval  7325  ord1eln01  8508  omlimcl  8590  brinxper  8751  ssfi  9192  funsnfsupp  9388  ltrnq  11068  ltsrpr  11166  difelfznle  13780  nelfzo  13803  modaddid  14054  muladdmodid  14057  modmulmodr  14084  modsumfzodifsn  14091  ccatsymb  14732  swrdnd0  14812  pfxsuffeqwrdeq  14852  pfxccatin12lem2a  14881  repswswrd  14940  cshwidxm  14964  s3iunsndisj  15127  lcmftp  16817  ncoprmlnprm  16910  modprm0  16989  dvdsprmpweqle  17070  difsqpwdvds  17071  brssc  17995  resmgmhm  18906  mgmhmco  18909  resmhm  19022  mhmco  19025  idresefmnd  19101  gasubg  19522  idrespermg  19631  rnghmco  20693  rhmco  20745  resrhm  20859  cply1mul  22620  dmatmul  22818  scmatf1  22852  slesolinv  23004  slesolinvbi  23005  slesolex  23006  cramerimplem3  23009  cramerimp  23010  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  bwth  23734  nmhmco  25081  chpchtsum  27552  gausslemma2dlem1a  27698  2lgslem1a1  27722  2sq2  27766  dchrisum0lem1  27849  subusgr  29876  isuvtx  29982  iscplgredg  30004  structtocusgr  30033  crctcshwlkn0  30416  crctcsh  30419  rusgrnumwwlk  30573  clwlkclwwlklem3  30598  clwwlkf1  30646  eucrctshift  30850  frgr3v  30882  frgrwopreglem5a  30918  numclwwlk3  30992  frgrreg  31001  ex-ceil  31055  occon2  31896  bnj1110  35659  satfv1lem  36214  relowlssretop  38380  poimirlem16  38648  poimirlem19  38651  poimirlem30  38662  omlimcl2  44338  pr2cv  44643  itgspltprt  47083  or2expropbilem1  48196  addmodne  48514  m1modmmod  48528  mod2addne  48534  iccpartiltu  48598  iccpartgt  48603  ich2exprop  48647  nprmmul2  48704  goldbachthlem1  48724  goldbachthlem2  48725  nn0e  48889  nneven  48890  stgoldbwt  48968  bgoldbtbndlem3  48999  bgoldbtbndlem4  49000  bgoldbtbnd  49001  isubgruhgr  49060  gricushgr  49109  isubgr3stgrlem7  49164  gpgedgvtx1  49254  ztprmneprm  49553  nn0sumltlt  49556  ldepspr  49679  blennngt2o2  49798  line2xlem  49959  aacllem  51108