Theorem anim12ci 616

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anim1ci  618  2exeuv  2694  2exeu  2708  2rexreu  3701  ideqg  5686  dfco2a  6066  frnssb  6862  fliftval  7048  omlimcl  8187  funsnfsupp  8841  ltrnq  10390  ltsrpr  10488  difelfznle  13016  nelfzo  13038  muladdmodid  13274  modmulmodr  13300  modsumfzodifsn  13307  ccatsymb  13927  swrdnd0  14010  pfxsuffeqwrdeq  14051  pfxccatin12lem2a  14080  repswswrd  14137  cshwidxm  14161  s3iunsndisj  14319  lcmftp  15970  ncoprmlnprm  16058  modprm0  16132  dvdsprmpweqle  16212  difsqpwdvds  16213  brssc  17076  resmhm  17977  mhmco  17980  idresefmnd  18056  gasubg  18424  idrespermg  18531  rhmco  19485  resrhm  19557  cply1mul  20923  dmatmul  21102  scmatf1  21136  slesolinv  21285  slesolinvbi  21286  slesolex  21287  cramerimplem3  21290  cramerimp  21291  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  bwth  22015  nmhmco  23362  chpchtsum  25803  gausslemma2dlem1a  25949  2lgslem1a1  25973  2sq2  26017  dchrisum0lem1  26100  subusgr  27079  isuvtx  27185  iscplgredg  27207  structtocusgr  27236  crctcshwlkn0  27607  crctcsh  27610  rusgrnumwwlk  27761  clwlkclwwlklem3  27786  clwwlkf1  27834  eucrctshift  28028  frgr3v  28060  frgrwopreglem5a  28096  numclwwlk3  28170  frgrreg  28179  ex-ceil  28233  occon2  29071  bnj1110  32364  satfv1lem  32722  relowlssretop  34780  poimirlem16  35073  poimirlem19  35076  poimirlem30  35087  pr2cv  40247  itgspltprt  42621  or2expropbilem1  43624  iccpartiltu  43939  iccpartgt  43944  ich2exprop  43988  goldbachthlem1  44062  goldbachthlem2  44063  nn0e  44215  nneven  44216  stgoldbwt  44294  bgoldbtbndlem3  44325  bgoldbtbndlem4  44326  bgoldbtbnd  44327  isomushgr  44344  isomuspgrlem1  44345  resmgmhm  44418  mgmhmco  44421  rnghmco  44531  ztprmneprm  44749  nn0sumltlt  44752  ldepspr  44882  m1modmmod  44935  blennngt2o2  45006  line2xlem  45167  aacllem  45329