Theorem anim12ci 615

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anim1ci  617  2exeuv  2629  2exeu  2643  2rexreu  3759  ideqg  5852  dfco2a  6246  fcdmssb  7121  fliftval  7313  ord1eln01  8496  omlimcl  8578  ssfi  9173  funsnfsupp  9387  ltrnq  10974  ltsrpr  11072  difelfznle  13615  nelfzo  13637  muladdmodid  13876  modmulmodr  13902  modsumfzodifsn  13909  ccatsymb  14532  swrdnd0  14607  pfxsuffeqwrdeq  14648  pfxccatin12lem2a  14677  repswswrd  14734  cshwidxm  14758  s3iunsndisj  14915  lcmftp  16573  ncoprmlnprm  16664  modprm0  16738  dvdsprmpweqle  16819  difsqpwdvds  16820  brssc  17761  resmhm  18701  mhmco  18704  idresefmnd  18780  gasubg  19166  idrespermg  19279  rhmco  20276  resrhm  20348  cply1mul  21818  dmatmul  21999  scmatf1  22033  slesolinv  22182  slesolinvbi  22183  slesolex  22184  cramerimplem3  22187  cramerimp  22188  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  bwth  22914  nmhmco  24273  chpchtsum  26722  gausslemma2dlem1a  26868  2lgslem1a1  26892  2sq2  26936  dchrisum0lem1  27019  subusgr  28546  isuvtx  28652  iscplgredg  28674  structtocusgr  28703  crctcshwlkn0  29075  crctcsh  29078  rusgrnumwwlk  29229  clwlkclwwlklem3  29254  clwwlkf1  29302  eucrctshift  29496  frgr3v  29528  frgrwopreglem5a  29564  numclwwlk3  29638  frgrreg  29647  ex-ceil  29701  occon2  30541  bnj1110  33993  satfv1lem  34353  relowlssretop  36244  poimirlem16  36504  poimirlem19  36507  poimirlem30  36518  omlimcl2  41991  pr2cv  42299  itgspltprt  44695  or2expropbilem1  45742  iccpartiltu  46090  iccpartgt  46095  ich2exprop  46139  goldbachthlem1  46213  goldbachthlem2  46214  nn0e  46365  nneven  46366  stgoldbwt  46444  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  bgoldbtbnd  46477  isomushgr  46494  isomuspgrlem1  46495  resmgmhm  46568  mgmhmco  46571  rnghmco  46706  ztprmneprm  47023  nn0sumltlt  47026  ldepspr  47154  m1modmmod  47207  blennngt2o2  47278  line2xlem  47439  aacllem  47848