Theorem anim12ci 626

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim1ci  628  2exeuv  2663  2exeu  2677  2rexreu  3728  ideqg  5842  dfco2a  6252  fcdmssb  7124  fliftval  7325  ord1eln01  8490  omlimcl  8572  brinxper  8733  ssfi  9167  funsnfsupp  9362  ltrnq  10982  ltsrpr  11080  difelfznle  13689  nelfzo  13712  modaddid  13963  muladdmodid  13966  modmulmodr  13993  modsumfzodifsn  14000  ccatsymb  14640  swrdnd0  14719  pfxsuffeqwrdeq  14759  pfxccatin12lem2a  14788  repswswrd  14847  cshwidxm  14871  s3iunsndisj  15031  lcmftp  16719  ncoprmlnprm  16812  modprm0  16890  dvdsprmpweqle  16971  difsqpwdvds  16972  brssc  17896  resmgmhm  18798  mgmhmco  18801  resmhm  18910  mhmco  18913  idresefmnd  18989  gasubg  19403  idrespermg  19512  rnghmco  20572  rhmco  20624  resrhm  20737  cply1mul  22493  dmatmul  22691  scmatf1  22725  slesolinv  22874  slesolinvbi  22875  slesolex  22876  cramerimplem3  22879  cramerimp  22880  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  bwth  23604  nmhmco  24950  chpchtsum  27420  gausslemma2dlem1a  27566  2lgslem1a1  27590  2sq2  27634  dchrisum0lem1  27717  subusgr  29676  isuvtx  29782  iscplgredg  29804  structtocusgr  29833  crctcshwlkn0  30207  crctcsh  30210  rusgrnumwwlk  30364  clwlkclwwlklem3  30389  clwwlkf1  30437  eucrctshift  30631  frgr3v  30663  frgrwopreglem5a  30699  numclwwlk3  30773  frgrreg  30782  ex-ceil  30836  occon2  31677  bnj1110  35402  satfv1lem  35875  relowlssretop  38050  poimirlem16  38328  poimirlem19  38331  poimirlem30  38342  omlimcl2  44010  pr2cv  44315  itgspltprt  46734  or2expropbilem1  47810  addmodne  48128  m1modmmod  48142  mod2addne  48148  iccpartiltu  48212  iccpartgt  48217  ich2exprop  48261  nprmmul2  48318  goldbachthlem1  48338  goldbachthlem2  48339  nn0e  48503  nneven  48504  stgoldbwt  48582  bgoldbtbndlem3  48613  bgoldbtbndlem4  48614  bgoldbtbnd  48615  isubgruhgr  48674  gricushgr  48723  isubgr3stgrlem7  48778  gpgedgvtx1  48868  ztprmneprm  49168  nn0sumltlt  49171  ldepspr  49294  blennngt2o2  49413  line2xlem  49574  aacllem  50662