Theorem anim12ci 613

Description: Variant of anim12i 612 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 612	. 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 206  df-an 396

This theorem is referenced by:  anim1ci  615  2exeuv  2635  2exeu  2649  2rexreu  3700  ideqg  5757  dfco2a  6147  frnssb  6989  fliftval  7180  omlimcl  8385  ssfi  8921  funsnfsupp  9113  ltrnq  10719  ltsrpr  10817  difelfznle  13352  nelfzo  13374  muladdmodid  13612  modmulmodr  13638  modsumfzodifsn  13645  ccatsymb  14268  swrdnd0  14351  pfxsuffeqwrdeq  14392  pfxccatin12lem2a  14421  repswswrd  14478  cshwidxm  14502  s3iunsndisj  14660  lcmftp  16322  ncoprmlnprm  16413  modprm0  16487  dvdsprmpweqle  16568  difsqpwdvds  16569  brssc  17507  resmhm  18440  mhmco  18443  idresefmnd  18519  gasubg  18889  idrespermg  19000  rhmco  19962  resrhm  20034  cply1mul  21446  dmatmul  21627  scmatf1  21661  slesolinv  21810  slesolinvbi  21811  slesolex  21812  cramerimplem3  21815  cramerimp  21816  chfacfscmulgsum  21990  chfacfpmmulgsum  21994  bwth  22542  nmhmco  23901  chpchtsum  26348  gausslemma2dlem1a  26494  2lgslem1a1  26518  2sq2  26562  dchrisum0lem1  26645  subusgr  27637  isuvtx  27743  iscplgredg  27765  structtocusgr  27794  crctcshwlkn0  28165  crctcsh  28168  rusgrnumwwlk  28319  clwlkclwwlklem3  28344  clwwlkf1  28392  eucrctshift  28586  frgr3v  28618  frgrwopreglem5a  28654  numclwwlk3  28728  frgrreg  28737  ex-ceil  28791  occon2  29629  bnj1110  32941  satfv1lem  33303  relowlssretop  35513  poimirlem16  35772  poimirlem19  35775  poimirlem30  35786  pr2cv  41108  itgspltprt  43474  or2expropbilem1  44477  iccpartiltu  44826  iccpartgt  44831  ich2exprop  44875  goldbachthlem1  44949  goldbachthlem2  44950  nn0e  45101  nneven  45102  stgoldbwt  45180  bgoldbtbndlem3  45211  bgoldbtbndlem4  45212  bgoldbtbnd  45213  isomushgr  45230  isomuspgrlem1  45231  resmgmhm  45304  mgmhmco  45307  rnghmco  45417  ztprmneprm  45635  nn0sumltlt  45638  ldepspr  45766  m1modmmod  45819  blennngt2o2  45890  line2xlem  46051  aacllem  46457