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  3724  ideqg  5798  dfco2a  6199  fcdmssb  7060  fliftval  7257  ord1eln01  8421  omlimcl  8503  brinxper  8661  ssfi  9097  funsnfsupp  9301  ltrnq  10892  ltsrpr  10990  difelfznle  13563  nelfzo  13585  modaddid  13832  muladdmodid  13835  modmulmodr  13862  modsumfzodifsn  13869  ccatsymb  14507  swrdnd0  14582  pfxsuffeqwrdeq  14622  pfxccatin12lem2a  14651  repswswrd  14708  cshwidxm  14732  s3iunsndisj  14893  lcmftp  16565  ncoprmlnprm  16657  modprm0  16735  dvdsprmpweqle  16816  difsqpwdvds  16817  brssc  17739  resmgmhm  18603  mgmhmco  18606  resmhm  18712  mhmco  18715  idresefmnd  18791  gasubg  19199  idrespermg  19308  rnghmco  20360  rhmco  20404  resrhm  20504  cply1mul  22199  dmatmul  22400  scmatf1  22434  slesolinv  22583  slesolinvbi  22584  slesolex  22585  cramerimplem3  22588  cramerimp  22589  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  bwth  23313  nmhmco  24660  chpchtsum  27146  gausslemma2dlem1a  27292  2lgslem1a1  27316  2sq2  27360  dchrisum0lem1  27443  subusgr  29252  isuvtx  29358  iscplgredg  29380  structtocusgr  29409  crctcshwlkn0  29784  crctcsh  29787  rusgrnumwwlk  29938  clwlkclwwlklem3  29963  clwwlkf1  30011  eucrctshift  30205  frgr3v  30237  frgrwopreglem5a  30273  numclwwlk3  30347  frgrreg  30356  ex-ceil  30410  occon2  31250  bnj1110  34951  satfv1lem  35337  relowlssretop  37339  poimirlem16  37618  poimirlem19  37621  poimirlem30  37632  omlimcl2  43218  pr2cv  43524  itgspltprt  45964  or2expropbilem1  47020  addmodne  47332  m1modmmod  47346  mod2addne  47352  iccpartiltu  47410  iccpartgt  47415  ich2exprop  47459  goldbachthlem1  47533  goldbachthlem2  47534  nn0e  47685  nneven  47686  stgoldbwt  47764  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  bgoldbtbnd  47797  isubgruhgr  47856  gricushgr  47905  isubgr3stgrlem7  47960  gpgedgvtx1  48050  ztprmneprm  48335  nn0sumltlt  48338  ldepspr  48462  blennngt2o2  48581  line2xlem  48742  aacllem  49790