Theorem anim12ci 620

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anim1ci  622  2exeuv  2636  2exeu  2650  2rexreu  3710  ideqg  5800  dfco2a  6204  fcdmssb  7070  fliftval  7267  ord1eln01  8428  omlimcl  8510  brinxper  8670  ssfi  9104  funsnfsupp  9302  ltrnq  10900  ltsrpr  10998  difelfznle  13594  nelfzo  13617  modaddid  13867  muladdmodid  13870  modmulmodr  13897  modsumfzodifsn  13904  ccatsymb  14543  swrdnd0  14618  pfxsuffeqwrdeq  14658  pfxccatin12lem2a  14687  repswswrd  14744  cshwidxm  14768  s3iunsndisj  14928  lcmftp  16603  ncoprmlnprm  16696  modprm0  16774  dvdsprmpweqle  16855  difsqpwdvds  16856  brssc  17779  resmgmhm  18677  mgmhmco  18680  resmhm  18786  mhmco  18789  idresefmnd  18865  gasubg  19275  idrespermg  19384  rnghmco  20435  rhmco  20479  resrhm  20580  cply1mul  22289  dmatmul  22487  scmatf1  22521  slesolinv  22670  slesolinvbi  22671  slesolex  22672  cramerimplem3  22675  cramerimp  22676  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  bwth  23400  nmhmco  24746  chpchtsum  27207  gausslemma2dlem1a  27353  2lgslem1a1  27377  2sq2  27421  dchrisum0lem1  27504  subusgr  29383  isuvtx  29489  iscplgredg  29511  structtocusgr  29540  crctcshwlkn0  29914  crctcsh  29917  rusgrnumwwlk  30071  clwlkclwwlklem3  30096  clwwlkf1  30144  eucrctshift  30338  frgr3v  30370  frgrwopreglem5a  30406  numclwwlk3  30480  frgrreg  30489  ex-ceil  30543  occon2  31384  bnj1110  35171  satfv1lem  35597  relowlssretop  37732  poimirlem16  38010  poimirlem19  38013  poimirlem30  38024  omlimcl2  43694  pr2cv  43999  itgspltprt  46429  or2expropbilem1  47502  addmodne  47820  m1modmmod  47834  mod2addne  47840  iccpartiltu  47904  iccpartgt  47909  ich2exprop  47953  nprmmul2  48010  goldbachthlem1  48030  goldbachthlem2  48031  nn0e  48195  nneven  48196  stgoldbwt  48274  bgoldbtbndlem3  48305  bgoldbtbndlem4  48306  bgoldbtbnd  48307  isubgruhgr  48366  gricushgr  48415  isubgr3stgrlem7  48470  gpgedgvtx1  48560  ztprmneprm  48845  nn0sumltlt  48848  ldepspr  48971  blennngt2o2  49090  line2xlem  49251  aacllem  50298