Theorem anim12ci 615

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  anim1ci  617  2exeuv  2632  2exeu  2646  2rexreu  3702  ideqg  5773  dfco2a  6164  fcdmssb  7027  fliftval  7219  ord1eln01  8357  omlimcl  8440  ssfi  8994  funsnfsupp  9196  ltrnq  10781  ltsrpr  10879  difelfznle  13416  nelfzo  13438  muladdmodid  13677  modmulmodr  13703  modsumfzodifsn  13710  ccatsymb  14332  swrdnd0  14415  pfxsuffeqwrdeq  14456  pfxccatin12lem2a  14485  repswswrd  14542  cshwidxm  14566  s3iunsndisj  14724  lcmftp  16386  ncoprmlnprm  16477  modprm0  16551  dvdsprmpweqle  16632  difsqpwdvds  16633  brssc  17571  resmhm  18504  mhmco  18507  idresefmnd  18583  gasubg  18953  idrespermg  19064  rhmco  20026  resrhm  20098  cply1mul  21510  dmatmul  21691  scmatf1  21725  slesolinv  21874  slesolinvbi  21875  slesolex  21876  cramerimplem3  21879  cramerimp  21880  chfacfscmulgsum  22054  chfacfpmmulgsum  22058  bwth  22606  nmhmco  23965  chpchtsum  26412  gausslemma2dlem1a  26558  2lgslem1a1  26582  2sq2  26626  dchrisum0lem1  26709  subusgr  27701  isuvtx  27807  iscplgredg  27829  structtocusgr  27858  crctcshwlkn0  28231  crctcsh  28234  rusgrnumwwlk  28385  clwlkclwwlklem3  28410  clwwlkf1  28458  eucrctshift  28652  frgr3v  28684  frgrwopreglem5a  28720  numclwwlk3  28794  frgrreg  28803  ex-ceil  28857  occon2  29695  bnj1110  33007  satfv1lem  33369  relowlssretop  35578  poimirlem16  35837  poimirlem19  35840  poimirlem30  35851  pr2cv  41193  itgspltprt  43569  or2expropbilem1  44584  iccpartiltu  44932  iccpartgt  44937  ich2exprop  44981  goldbachthlem1  45055  goldbachthlem2  45056  nn0e  45207  nneven  45208  stgoldbwt  45286  bgoldbtbndlem3  45317  bgoldbtbndlem4  45318  bgoldbtbnd  45319  isomushgr  45336  isomuspgrlem1  45337  resmgmhm  45410  mgmhmco  45413  rnghmco  45523  ztprmneprm  45741  nn0sumltlt  45744  ldepspr  45872  m1modmmod  45925  blennngt2o2  45996  line2xlem  46157  aacllem  46563