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  3722  ideqg  5808  dfco2a  6212  fcdmssb  7076  fliftval  7272  ord1eln01  8433  omlimcl  8515  brinxper  8675  ssfi  9109  funsnfsupp  9307  ltrnq  10902  ltsrpr  11000  difelfznle  13570  nelfzo  13592  modaddid  13842  muladdmodid  13845  modmulmodr  13872  modsumfzodifsn  13879  ccatsymb  14518  swrdnd0  14593  pfxsuffeqwrdeq  14633  pfxccatin12lem2a  14662  repswswrd  14719  cshwidxm  14743  s3iunsndisj  14903  lcmftp  16575  ncoprmlnprm  16667  modprm0  16745  dvdsprmpweqle  16826  difsqpwdvds  16827  brssc  17750  resmgmhm  18648  mgmhmco  18651  resmhm  18757  mhmco  18760  idresefmnd  18836  gasubg  19243  idrespermg  19352  rnghmco  20405  rhmco  20446  resrhm  20546  cply1mul  22252  dmatmul  22453  scmatf1  22487  slesolinv  22636  slesolinvbi  22637  slesolex  22638  cramerimplem3  22641  cramerimp  22642  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  bwth  23366  nmhmco  24712  chpchtsum  27198  gausslemma2dlem1a  27344  2lgslem1a1  27368  2sq2  27412  dchrisum0lem1  27495  subusgr  29374  isuvtx  29480  iscplgredg  29502  structtocusgr  29531  crctcshwlkn0  29906  crctcsh  29909  rusgrnumwwlk  30063  clwlkclwwlklem3  30088  clwwlkf1  30136  eucrctshift  30330  frgr3v  30362  frgrwopreglem5a  30398  numclwwlk3  30472  frgrreg  30481  ex-ceil  30535  occon2  31375  bnj1110  35157  satfv1lem  35575  relowlssretop  37615  poimirlem16  37884  poimirlem19  37887  poimirlem30  37898  omlimcl2  43596  pr2cv  43901  itgspltprt  46334  or2expropbilem1  47389  addmodne  47701  m1modmmod  47715  mod2addne  47721  iccpartiltu  47779  iccpartgt  47784  ich2exprop  47828  goldbachthlem1  47902  goldbachthlem2  47903  nn0e  48054  nneven  48055  stgoldbwt  48133  bgoldbtbndlem3  48164  bgoldbtbndlem4  48165  bgoldbtbnd  48166  isubgruhgr  48225  gricushgr  48274  isubgr3stgrlem7  48329  gpgedgvtx1  48419  ztprmneprm  48704  nn0sumltlt  48707  ldepspr  48830  blennngt2o2  48949  line2xlem  49110  aacllem  50157