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  2659  2exeu  2673  2rexreu  3723  ideqg  5835  dfco2a  6246  fcdmssb  7119  fliftval  7321  ord1eln01  8487  omlimcl  8569  brinxper  8730  ssfi  9171  funsnfsupp  9366  ltrnq  10992  ltsrpr  11090  difelfznle  13701  nelfzo  13724  modaddid  13975  muladdmodid  13978  modmulmodr  14005  modsumfzodifsn  14012  ccatsymb  14652  swrdnd0  14731  pfxsuffeqwrdeq  14771  pfxccatin12lem2a  14800  repswswrd  14859  cshwidxm  14883  s3iunsndisj  15045  lcmftp  16732  ncoprmlnprm  16825  modprm0  16903  dvdsprmpweqle  16984  difsqpwdvds  16985  brssc  17909  resmgmhm  18819  mgmhmco  18822  resmhm  18935  mhmco  18938  idresefmnd  19014  gasubg  19435  idrespermg  19544  rnghmco  20604  rhmco  20656  resrhm  20769  cply1mul  22527  dmatmul  22725  scmatf1  22759  slesolinv  22911  slesolinvbi  22912  slesolex  22913  cramerimplem3  22916  cramerimp  22917  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  bwth  23641  nmhmco  24988  chpchtsum  27463  gausslemma2dlem1a  27609  2lgslem1a1  27633  2sq2  27677  dchrisum0lem1  27760  subusgr  29757  isuvtx  29863  iscplgredg  29885  structtocusgr  29914  crctcshwlkn0  30297  crctcsh  30300  rusgrnumwwlk  30454  clwlkclwwlklem3  30479  clwwlkf1  30527  eucrctshift  30731  frgr3v  30763  frgrwopreglem5a  30799  numclwwlk3  30873  frgrreg  30882  ex-ceil  30936  occon2  31777  bnj1110  35499  satfv1lem  35949  relowlssretop  38125  poimirlem16  38393  poimirlem19  38396  poimirlem30  38407  omlimcl2  44091  pr2cv  44396  itgspltprt  46815  or2expropbilem1  47928  addmodne  48246  m1modmmod  48260  mod2addne  48266  iccpartiltu  48330  iccpartgt  48335  ich2exprop  48379  nprmmul2  48436  goldbachthlem1  48456  goldbachthlem2  48457  nn0e  48621  nneven  48622  stgoldbwt  48700  bgoldbtbndlem3  48731  bgoldbtbndlem4  48732  bgoldbtbnd  48733  isubgruhgr  48792  gricushgr  48841  isubgr3stgrlem7  48896  gpgedgvtx1  48986  ztprmneprm  49285  nn0sumltlt  49288  ldepspr  49411  blennngt2o2  49530  line2xlem  49691  aacllem  50780