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  2627  2exeu  2641  2rexreu  3721  ideqg  5791  dfco2a  6193  fcdmssb  7055  fliftval  7250  ord1eln01  8411  omlimcl  8493  brinxper  8651  ssfi  9082  funsnfsupp  9276  ltrnq  10870  ltsrpr  10968  difelfznle  13542  nelfzo  13564  modaddid  13814  muladdmodid  13817  modmulmodr  13844  modsumfzodifsn  13851  ccatsymb  14490  swrdnd0  14565  pfxsuffeqwrdeq  14605  pfxccatin12lem2a  14634  repswswrd  14691  cshwidxm  14715  s3iunsndisj  14875  lcmftp  16547  ncoprmlnprm  16639  modprm0  16717  dvdsprmpweqle  16798  difsqpwdvds  16799  brssc  17721  resmgmhm  18619  mgmhmco  18622  resmhm  18728  mhmco  18731  idresefmnd  18807  gasubg  19215  idrespermg  19324  rnghmco  20376  rhmco  20417  resrhm  20517  cply1mul  22212  dmatmul  22413  scmatf1  22447  slesolinv  22596  slesolinvbi  22597  slesolex  22598  cramerimplem3  22601  cramerimp  22602  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  bwth  23326  nmhmco  24672  chpchtsum  27158  gausslemma2dlem1a  27304  2lgslem1a1  27328  2sq2  27372  dchrisum0lem1  27455  subusgr  29268  isuvtx  29374  iscplgredg  29396  structtocusgr  29425  crctcshwlkn0  29800  crctcsh  29803  rusgrnumwwlk  29954  clwlkclwwlklem3  29979  clwwlkf1  30027  eucrctshift  30221  frgr3v  30253  frgrwopreglem5a  30289  numclwwlk3  30363  frgrreg  30372  ex-ceil  30426  occon2  31266  bnj1110  34992  satfv1lem  35404  relowlssretop  37403  poimirlem16  37682  poimirlem19  37685  poimirlem30  37696  omlimcl2  43281  pr2cv  43587  itgspltprt  46023  or2expropbilem1  47069  addmodne  47381  m1modmmod  47395  mod2addne  47401  iccpartiltu  47459  iccpartgt  47464  ich2exprop  47508  goldbachthlem1  47582  goldbachthlem2  47583  nn0e  47734  nneven  47735  stgoldbwt  47813  bgoldbtbndlem3  47844  bgoldbtbndlem4  47845  bgoldbtbnd  47846  isubgruhgr  47905  gricushgr  47954  isubgr3stgrlem7  48009  gpgedgvtx1  48099  ztprmneprm  48384  nn0sumltlt  48387  ldepspr  48511  blennngt2o2  48630  line2xlem  48791  aacllem  49839