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  3758  ideqg  5850  dfco2a  6243  fcdmssb  7118  fliftval  7310  ord1eln01  8493  omlimcl  8575  ssfi  9170  funsnfsupp  9384  ltrnq  10971  ltsrpr  11069  difelfznle  13612  nelfzo  13634  muladdmodid  13873  modmulmodr  13899  modsumfzodifsn  13906  ccatsymb  14529  swrdnd0  14604  pfxsuffeqwrdeq  14645  pfxccatin12lem2a  14674  repswswrd  14731  cshwidxm  14755  s3iunsndisj  14912  lcmftp  16570  ncoprmlnprm  16661  modprm0  16735  dvdsprmpweqle  16816  difsqpwdvds  16817  brssc  17758  resmhm  18698  mhmco  18701  idresefmnd  18777  gasubg  19161  idrespermg  19274  rhmco  20269  resrhm  20386  cply1mul  21810  dmatmul  21991  scmatf1  22025  slesolinv  22174  slesolinvbi  22175  slesolex  22176  cramerimplem3  22179  cramerimp  22180  chfacfscmulgsum  22354  chfacfpmmulgsum  22358  bwth  22906  nmhmco  24265  chpchtsum  26712  gausslemma2dlem1a  26858  2lgslem1a1  26882  2sq2  26926  dchrisum0lem1  27009  subusgr  28536  isuvtx  28642  iscplgredg  28664  structtocusgr  28693  crctcshwlkn0  29065  crctcsh  29068  rusgrnumwwlk  29219  clwlkclwwlklem3  29244  clwwlkf1  29292  eucrctshift  29486  frgr3v  29518  frgrwopreglem5a  29554  numclwwlk3  29628  frgrreg  29637  ex-ceil  29691  occon2  30529  bnj1110  33982  satfv1lem  34342  relowlssretop  36233  poimirlem16  36493  poimirlem19  36496  poimirlem30  36507  omlimcl2  41977  pr2cv  42285  itgspltprt  44682  or2expropbilem1  45729  iccpartiltu  46077  iccpartgt  46082  ich2exprop  46126  goldbachthlem1  46200  goldbachthlem2  46201  nn0e  46352  nneven  46353  stgoldbwt  46431  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  bgoldbtbnd  46464  isomushgr  46481  isomuspgrlem1  46482  resmgmhm  46555  mgmhmco  46558  rnghmco  46692  ztprmneprm  46977  nn0sumltlt  46980  ldepspr  47108  m1modmmod  47161  blennngt2o2  47232  line2xlem  47393  aacllem  47802