Theorem anim12ci 625

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anim1ci  627  2exeuv  2662  2exeu  2676  2rexreu  3728  ideqg  5827  dfco2a  6236  fcdmssb  7107  fliftval  7304  ord1eln01  8469  omlimcl  8551  brinxper  8712  ssfi  9145  funsnfsupp  9340  ltrnq  10952  ltsrpr  11050  difelfznle  13658  nelfzo  13681  modaddid  13931  muladdmodid  13934  modmulmodr  13961  modsumfzodifsn  13968  ccatsymb  14608  swrdnd0  14683  pfxsuffeqwrdeq  14723  pfxccatin12lem2a  14752  repswswrd  14809  cshwidxm  14833  s3iunsndisj  14993  lcmftp  16682  ncoprmlnprm  16775  modprm0  16853  dvdsprmpweqle  16934  difsqpwdvds  16935  brssc  17859  resmgmhm  18757  mgmhmco  18760  resmhm  18867  mhmco  18870  idresefmnd  18946  gasubg  19360  idrespermg  19469  rnghmco  20527  rhmco  20571  resrhm  20674  cply1mul  22413  dmatmul  22611  scmatf1  22645  slesolinv  22794  slesolinvbi  22795  slesolex  22796  cramerimplem3  22799  cramerimp  22800  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  bwth  23524  nmhmco  24870  chpchtsum  27337  gausslemma2dlem1a  27483  2lgslem1a1  27507  2sq2  27551  dchrisum0lem1  27634  subusgr  29544  isuvtx  29650  iscplgredg  29672  structtocusgr  29701  crctcshwlkn0  30075  crctcsh  30078  rusgrnumwwlk  30232  clwlkclwwlklem3  30257  clwwlkf1  30305  eucrctshift  30499  frgr3v  30531  frgrwopreglem5a  30567  numclwwlk3  30641  frgrreg  30650  ex-ceil  30704  occon2  31545  bnj1110  35282  satfv1lem  35720  relowlssretop  37864  poimirlem16  38142  poimirlem19  38145  poimirlem30  38156  omlimcl2  43826  pr2cv  44131  itgspltprt  46552  or2expropbilem1  47625  addmodne  47943  m1modmmod  47957  mod2addne  47963  iccpartiltu  48027  iccpartgt  48032  ich2exprop  48076  nprmmul2  48133  goldbachthlem1  48153  goldbachthlem2  48154  nn0e  48318  nneven  48319  stgoldbwt  48397  bgoldbtbndlem3  48428  bgoldbtbndlem4  48429  bgoldbtbnd  48430  isubgruhgr  48489  gricushgr  48538  isubgr3stgrlem7  48593  gpgedgvtx1  48683  ztprmneprm  48979  nn0sumltlt  48982  ldepspr  49105  blennngt2o2  49224  line2xlem  49385  aacllem  50431