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  2658  2exeu  2672  2rexreu  3720  ideqg  5829  dfco2a  6240  fcdmssb  7114  fliftval  7316  ord1eln01  8488  omlimcl  8570  brinxper  8731  ssfi  9172  funsnfsupp  9368  ltrnq  11045  ltsrpr  11143  difelfznle  13756  nelfzo  13779  modaddid  14030  muladdmodid  14033  modmulmodr  14060  modsumfzodifsn  14067  ccatsymb  14708  swrdnd0  14787  pfxsuffeqwrdeq  14827  pfxccatin12lem2a  14856  repswswrd  14915  cshwidxm  14939  s3iunsndisj  15101  lcmftp  16791  ncoprmlnprm  16884  modprm0  16963  dvdsprmpweqle  17044  difsqpwdvds  17045  brssc  17969  resmgmhm  18880  mgmhmco  18883  resmhm  18996  mhmco  18999  idresefmnd  19075  gasubg  19496  idrespermg  19605  rnghmco  20667  rhmco  20719  resrhm  20833  cply1mul  22594  dmatmul  22792  scmatf1  22826  slesolinv  22978  slesolinvbi  22979  slesolex  22980  cramerimplem3  22983  cramerimp  22984  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  bwth  23708  nmhmco  25055  chpchtsum  27528  gausslemma2dlem1a  27674  2lgslem1a1  27698  2sq2  27742  dchrisum0lem1  27825  subusgr  29852  isuvtx  29958  iscplgredg  29980  structtocusgr  30009  crctcshwlkn0  30392  crctcsh  30395  rusgrnumwwlk  30549  clwlkclwwlklem3  30574  clwwlkf1  30622  eucrctshift  30826  frgr3v  30858  frgrwopreglem5a  30894  numclwwlk3  30968  frgrreg  30977  ex-ceil  31031  occon2  31872  bnj1110  35595  satfv1lem  36096  relowlssretop  38254  poimirlem16  38522  poimirlem19  38525  poimirlem30  38536  omlimcl2  44202  pr2cv  44507  itgspltprt  46933  or2expropbilem1  48046  addmodne  48364  m1modmmod  48378  mod2addne  48384  iccpartiltu  48448  iccpartgt  48453  ich2exprop  48497  nprmmul2  48554  goldbachthlem1  48574  goldbachthlem2  48575  nn0e  48739  nneven  48740  stgoldbwt  48818  bgoldbtbndlem3  48849  bgoldbtbndlem4  48850  bgoldbtbnd  48851  isubgruhgr  48910  gricushgr  48959  isubgr3stgrlem7  49014  gpgedgvtx1  49104  ztprmneprm  49403  nn0sumltlt  49406  ldepspr  49529  blennngt2o2  49648  line2xlem  49809  aacllem  50883