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 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  617  2exeuv  2633  2exeu  2647  2rexreu  3709  ideqg  5800  dfco2a  6204  fcdmssb  7068  fliftval  7264  ord1eln01  8424  omlimcl  8506  brinxper  8666  ssfi  9100  funsnfsupp  9298  ltrnq  10893  ltsrpr  10991  difelfznle  13587  nelfzo  13610  modaddid  13860  muladdmodid  13863  modmulmodr  13890  modsumfzodifsn  13897  ccatsymb  14536  swrdnd0  14611  pfxsuffeqwrdeq  14651  pfxccatin12lem2a  14680  repswswrd  14737  cshwidxm  14761  s3iunsndisj  14921  lcmftp  16596  ncoprmlnprm  16689  modprm0  16767  dvdsprmpweqle  16848  difsqpwdvds  16849  brssc  17772  resmgmhm  18670  mgmhmco  18673  resmhm  18779  mhmco  18782  idresefmnd  18858  gasubg  19268  idrespermg  19377  rnghmco  20428  rhmco  20469  resrhm  20569  cply1mul  22271  dmatmul  22472  scmatf1  22506  slesolinv  22655  slesolinvbi  22656  slesolex  22657  cramerimplem3  22660  cramerimp  22661  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  bwth  23385  nmhmco  24731  chpchtsum  27196  gausslemma2dlem1a  27342  2lgslem1a1  27366  2sq2  27410  dchrisum0lem1  27493  subusgr  29372  isuvtx  29478  iscplgredg  29500  structtocusgr  29529  crctcshwlkn0  29904  crctcsh  29907  rusgrnumwwlk  30061  clwlkclwwlklem3  30086  clwwlkf1  30134  eucrctshift  30328  frgr3v  30360  frgrwopreglem5a  30396  numclwwlk3  30470  frgrreg  30479  ex-ceil  30533  occon2  31374  bnj1110  35140  satfv1lem  35560  relowlssretop  37693  poimirlem16  37971  poimirlem19  37974  poimirlem30  37985  omlimcl2  43688  pr2cv  43993  itgspltprt  46425  or2expropbilem1  47492  addmodne  47810  m1modmmod  47824  mod2addne  47830  iccpartiltu  47894  iccpartgt  47899  ich2exprop  47943  nprmmul2  48000  goldbachthlem1  48020  goldbachthlem2  48021  nn0e  48185  nneven  48186  stgoldbwt  48264  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  isubgruhgr  48356  gricushgr  48405  isubgr3stgrlem7  48460  gpgedgvtx1  48550  ztprmneprm  48835  nn0sumltlt  48838  ldepspr  48961  blennngt2o2  49080  line2xlem  49241  aacllem  50288