Theorem anim12ci 614

Description: Variant of anim12i 613 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 613	. 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  616  2exeuv  2625  2exeu  2639  2rexreu  3733  ideqg  5815  dfco2a  6219  fcdmssb  7094  fliftval  7291  ord1eln01  8460  omlimcl  8542  brinxper  8700  ssfi  9137  funsnfsupp  9343  ltrnq  10932  ltsrpr  11030  difelfznle  13603  nelfzo  13625  modaddid  13872  muladdmodid  13875  modmulmodr  13902  modsumfzodifsn  13909  ccatsymb  14547  swrdnd0  14622  pfxsuffeqwrdeq  14663  pfxccatin12lem2a  14692  repswswrd  14749  cshwidxm  14773  s3iunsndisj  14934  lcmftp  16606  ncoprmlnprm  16698  modprm0  16776  dvdsprmpweqle  16857  difsqpwdvds  16858  brssc  17776  resmgmhm  18638  mgmhmco  18641  resmhm  18747  mhmco  18750  idresefmnd  18826  gasubg  19234  idrespermg  19341  rnghmco  20366  rhmco  20410  resrhm  20510  cply1mul  22183  dmatmul  22384  scmatf1  22418  slesolinv  22567  slesolinvbi  22568  slesolex  22569  cramerimplem3  22572  cramerimp  22573  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  bwth  23297  nmhmco  24644  chpchtsum  27130  gausslemma2dlem1a  27276  2lgslem1a1  27300  2sq2  27344  dchrisum0lem1  27427  subusgr  29216  isuvtx  29322  iscplgredg  29344  structtocusgr  29373  crctcshwlkn0  29751  crctcsh  29754  rusgrnumwwlk  29905  clwlkclwwlklem3  29930  clwwlkf1  29978  eucrctshift  30172  frgr3v  30204  frgrwopreglem5a  30240  numclwwlk3  30314  frgrreg  30323  ex-ceil  30377  occon2  31217  bnj1110  34972  satfv1lem  35349  relowlssretop  37351  poimirlem16  37630  poimirlem19  37633  poimirlem30  37644  omlimcl2  43231  pr2cv  43537  itgspltprt  45977  or2expropbilem1  47033  addmodne  47345  m1modmmod  47359  mod2addne  47365  iccpartiltu  47423  iccpartgt  47428  ich2exprop  47472  goldbachthlem1  47546  goldbachthlem2  47547  nn0e  47698  nneven  47699  stgoldbwt  47777  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  isubgruhgr  47868  gricushgr  47917  isubgr3stgrlem7  47971  gpgedgvtx1  48053  ztprmneprm  48335  nn0sumltlt  48338  ldepspr  48462  blennngt2o2  48581  line2xlem  48742  aacllem  49790