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 207  df-an 396

This theorem is referenced by:  anim1ci  615  2exeuv  2635  2exeu  2649  2rexreu  3784  ideqg  5876  dfco2a  6277  fcdmssb  7156  fliftval  7352  ord1eln01  8552  omlimcl  8634  brinxper  8792  ssfi  9240  funsnfsupp  9461  ltrnq  11048  ltsrpr  11146  difelfznle  13699  nelfzo  13721  muladdmodid  13962  modmulmodr  13988  modsumfzodifsn  13995  ccatsymb  14630  swrdnd0  14705  pfxsuffeqwrdeq  14746  pfxccatin12lem2a  14775  repswswrd  14832  cshwidxm  14856  s3iunsndisj  15017  lcmftp  16683  ncoprmlnprm  16775  modprm0  16852  dvdsprmpweqle  16933  difsqpwdvds  16934  brssc  17875  resmgmhm  18749  mgmhmco  18752  resmhm  18855  mhmco  18858  idresefmnd  18934  gasubg  19342  idrespermg  19453  rnghmco  20483  rhmco  20527  resrhm  20629  cply1mul  22321  dmatmul  22524  scmatf1  22558  slesolinv  22707  slesolinvbi  22708  slesolex  22709  cramerimplem3  22712  cramerimp  22713  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  bwth  23439  nmhmco  24798  chpchtsum  27281  gausslemma2dlem1a  27427  2lgslem1a1  27451  2sq2  27495  dchrisum0lem1  27578  subusgr  29324  isuvtx  29430  iscplgredg  29452  structtocusgr  29481  crctcshwlkn0  29854  crctcsh  29857  rusgrnumwwlk  30008  clwlkclwwlklem3  30033  clwwlkf1  30081  eucrctshift  30275  frgr3v  30307  frgrwopreglem5a  30343  numclwwlk3  30417  frgrreg  30426  ex-ceil  30480  occon2  31320  bnj1110  34958  satfv1lem  35330  relowlssretop  37329  poimirlem16  37596  poimirlem19  37599  poimirlem30  37610  omlimcl2  43203  pr2cv  43510  itgspltprt  45900  or2expropbilem1  46947  iccpartiltu  47296  iccpartgt  47301  ich2exprop  47345  goldbachthlem1  47419  goldbachthlem2  47420  nn0e  47571  nneven  47572  stgoldbwt  47650  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  isubgruhgr  47738  gricushgr  47770  ztprmneprm  48072  nn0sumltlt  48075  ldepspr  48202  m1modmmod  48255  blennngt2o2  48326  line2xlem  48487  aacllem  48895