Theorem anim12ci 625

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anim1ci  627  2exeuv  2660  2exeu  2674  2rexreu  3726  ideqg  5839  dfco2a  6249  fcdmssb  7119  fliftval  7316  ord1eln01  8482  omlimcl  8564  brinxper  8725  ssfi  9158  funsnfsupp  9353  ltrnq  10965  ltsrpr  11063  difelfznle  13672  nelfzo  13695  modaddid  13945  muladdmodid  13948  modmulmodr  13975  modsumfzodifsn  13982  ccatsymb  14622  swrdnd0  14697  pfxsuffeqwrdeq  14737  pfxccatin12lem2a  14766  repswswrd  14823  cshwidxm  14847  s3iunsndisj  15007  lcmftp  16695  ncoprmlnprm  16788  modprm0  16866  dvdsprmpweqle  16947  difsqpwdvds  16948  brssc  17872  resmgmhm  18770  mgmhmco  18773  resmhm  18880  mhmco  18883  idresefmnd  18959  gasubg  19373  idrespermg  19482  rnghmco  20540  rhmco  20584  resrhm  20687  cply1mul  22437  dmatmul  22635  scmatf1  22669  slesolinv  22818  slesolinvbi  22819  slesolex  22820  cramerimplem3  22823  cramerimp  22824  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  bwth  23548  nmhmco  24894  chpchtsum  27364  gausslemma2dlem1a  27510  2lgslem1a1  27534  2sq2  27578  dchrisum0lem1  27661  subusgr  29620  isuvtx  29726  iscplgredg  29748  structtocusgr  29777  crctcshwlkn0  30151  crctcsh  30154  rusgrnumwwlk  30308  clwlkclwwlklem3  30333  clwwlkf1  30381  eucrctshift  30575  frgr3v  30607  frgrwopreglem5a  30643  numclwwlk3  30717  frgrreg  30726  ex-ceil  30780  occon2  31621  bnj1110  35351  satfv1lem  35835  relowlssretop  37990  poimirlem16  38268  poimirlem19  38271  poimirlem30  38282  omlimcl2  43952  pr2cv  44257  itgspltprt  46676  or2expropbilem1  47752  addmodne  48070  m1modmmod  48084  mod2addne  48090  iccpartiltu  48154  iccpartgt  48159  ich2exprop  48203  nprmmul2  48260  goldbachthlem1  48280  goldbachthlem2  48281  nn0e  48445  nneven  48446  stgoldbwt  48524  bgoldbtbndlem3  48555  bgoldbtbndlem4  48556  bgoldbtbnd  48557  isubgruhgr  48616  gricushgr  48665  isubgr3stgrlem7  48720  gpgedgvtx1  48810  ztprmneprm  49110  nn0sumltlt  49113  ldepspr  49236  blennngt2o2  49355  line2xlem  49516  aacllem  50584