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  2660  2exeu  2674  2rexreu  3723  ideqg  5836  dfco2a  6261  fcdmssb  7149  fliftval  7350  ord1eln01  8535  omlimcl  8617  brinxper  8778  ssfi  9219  funsnfsupp  9414  ltrnq  11094  ltsrpr  11192  difelfznle  13806  nelfzo  13829  modaddid  14080  muladdmodid  14083  modmulmodr  14110  modsumfzodifsn  14117  ccatsymb  14758  swrdnd0  14838  pfxsuffeqwrdeq  14878  pfxccatin12lem2a  14907  repswswrd  14966  cshwidxm  14990  s3iunsndisj  15153  lcmftp  16843  ncoprmlnprm  16936  modprm0  17015  dvdsprmpweqle  17096  difsqpwdvds  17097  brssc  18021  resmgmhm  18932  mgmhmco  18935  resmhm  19048  mhmco  19051  idresefmnd  19127  gasubg  19549  idrespermg  19658  rnghmco  20720  rhmco  20772  resrhm  20886  cply1mul  22647  dmatmul  22845  scmatf1  22879  slesolinv  23031  slesolinvbi  23032  slesolex  23033  cramerimplem3  23036  cramerimp  23037  chfacfscmulgsum  23211  chfacfpmmulgsum  23215  bwth  23761  nmhmco  25108  chpchtsum  27579  gausslemma2dlem1a  27725  2lgslem1a1  27749  2sq2  27793  dchrisum0lem1  27876  subusgr  29903  isuvtx  30009  iscplgredg  30031  structtocusgr  30060  crctcshwlkn0  30443  crctcsh  30446  rusgrnumwwlk  30600  clwlkclwwlklem3  30625  clwwlkf1  30673  eucrctshift  30877  frgr3v  30909  frgrwopreglem5a  30945  numclwwlk3  31019  frgrreg  31028  ex-ceil  31082  occon2  31923  bnj1110  35695  satfv1lem  36307  relowlssretop  38491  poimirlem16  38759  poimirlem19  38762  poimirlem30  38773  omlimcl2  44447  pr2cv  44752  itgspltprt  47204  or2expropbilem1  48317  addmodne  48635  m1modmmod  48649  mod2addne  48655  iccpartiltu  48719  iccpartgt  48724  ich2exprop  48768  nprmmul2  48825  goldbachthlem1  48845  goldbachthlem2  48846  nn0e  49010  nneven  49011  stgoldbwt  49089  bgoldbtbndlem3  49120  bgoldbtbndlem4  49121  bgoldbtbnd  49122  isubgruhgr  49181  gricushgr  49230  isubgr3stgrlem7  49285  gpgedgvtx1  49375  ztprmneprm  49674  nn0sumltlt  49677  ldepspr  49800  blennngt2o2  49919  line2xlem  50080  aacllem  51251