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  2630  2exeu  2644  2rexreu  3771  ideqg  5865  dfco2a  6268  fcdmssb  7142  fliftval  7336  ord1eln01  8533  omlimcl  8615  brinxper  8773  ssfi  9212  funsnfsupp  9430  ltrnq  11017  ltsrpr  11115  difelfznle  13679  nelfzo  13701  muladdmodid  13948  modmulmodr  13975  modsumfzodifsn  13982  ccatsymb  14617  swrdnd0  14692  pfxsuffeqwrdeq  14733  pfxccatin12lem2a  14762  repswswrd  14819  cshwidxm  14843  s3iunsndisj  15004  lcmftp  16670  ncoprmlnprm  16762  modprm0  16839  dvdsprmpweqle  16920  difsqpwdvds  16921  brssc  17862  resmgmhm  18737  mgmhmco  18740  resmhm  18846  mhmco  18849  idresefmnd  18925  gasubg  19333  idrespermg  19444  rnghmco  20474  rhmco  20518  resrhm  20618  cply1mul  22316  dmatmul  22519  scmatf1  22553  slesolinv  22702  slesolinvbi  22703  slesolex  22704  cramerimplem3  22707  cramerimp  22708  chfacfscmulgsum  22882  chfacfpmmulgsum  22886  bwth  23434  nmhmco  24793  chpchtsum  27278  gausslemma2dlem1a  27424  2lgslem1a1  27448  2sq2  27492  dchrisum0lem1  27575  subusgr  29321  isuvtx  29427  iscplgredg  29449  structtocusgr  29478  crctcshwlkn0  29851  crctcsh  29854  rusgrnumwwlk  30005  clwlkclwwlklem3  30030  clwwlkf1  30078  eucrctshift  30272  frgr3v  30304  frgrwopreglem5a  30340  numclwwlk3  30414  frgrreg  30423  ex-ceil  30477  occon2  31317  bnj1110  34975  satfv1lem  35347  relowlssretop  37346  poimirlem16  37623  poimirlem19  37626  poimirlem30  37637  omlimcl2  43231  pr2cv  43538  itgspltprt  45935  or2expropbilem1  46982  addmodne  47284  iccpartiltu  47347  iccpartgt  47352  ich2exprop  47396  goldbachthlem1  47470  goldbachthlem2  47471  nn0e  47622  nneven  47623  stgoldbwt  47701  bgoldbtbndlem3  47732  bgoldbtbndlem4  47733  bgoldbtbnd  47734  isubgruhgr  47792  gricushgr  47824  isubgr3stgrlem7  47875  gpgedgvtx1  47955  ztprmneprm  48192  nn0sumltlt  48195  ldepspr  48319  m1modmmod  48371  blennngt2o2  48442  line2xlem  48603  aacllem  49032