HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem an1rs 489
Description: Deduction rearranging conjuncts.
Hypothesis
Ref Expression
an1rs.1 |- (((ph /\ ps) /\ ch) -> th)
Assertion
Ref Expression
an1rs |- (((ph /\ ch) /\ ps) -> th)
Proof of Theorem an1rs
StepHypRef Expression
1 an23 485 . 2 |- (((ph /\ ch) /\ ps) <-> ((ph /\ ps) /\ ch))
2 an1rs.1 . 2 |- (((ph /\ ps) /\ ch) -> th)
31, 2sylbi 199 1 |- (((ph /\ ch) /\ ps) -> th)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  anabsan 504  ordunisssuc 3078  fssres 3634  foco 3673  f1ores 3694  fconstfv 3840  isocnv 3887  f1oiso 3895  oev2 4152  oaordi 4170  oaass 4185  omlimcl 4199  odi 4200  omass 4201  oewordri 4209  oelim2 4212  oaabs 4242  undom 4424  mapenlem1 4475  mapenlem2 4476  mapxpen 4481  mapunen 4488  isfinite2 4529  supmo 4556  unidom 4788  suplem1pr 5141  suplem2pr 5142  recexsrlem 5192  suppsr2 5203  cnegextlem3 5327  axsup 5487  xrlttrt 5534  recextlem2 5664  suprleub 6014  dfinfmr 6022  xrsupsslem 6031  xrinfmsslem 6032  supxr2 6037  supxrre 6038  supxrunb1 6044  supxrbnd1 6050  supxrbnd2 6051  supxrleub 6054  uzindOLD 6164  qrecclt 6219  iooss1 6318  iooss2 6319  fsequb 6463  recexpt 6534  divexpt 6538  expmwordit 6545  cau5i 6862  cvg3 6868  fsum2mul 6983  fsumcmpndx2 6988  climconst 7039  2climnn 7047  2climnn0 7048  climshft2 7051  iserzshft2 7052  climrecl 7055  climge0 7057  climcau 7100  caucvglem6 7106  cvgcmp3c 7130  isum1p 7149  isumreclt 7153  cvgratlem1 7193  cvgratlem2 7194  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag2 7202  fsum0diag3 7203  fsum0diag4 7204  infxpidmlem10 7512  infdif 7519  tgclt 7574  cldcls 7632  clsval2 7635  0ntr 7652  innei 7686  sncld 7737  bl2in 7795  blin 7804  metcnp 7839  metcn 7841  metcnp3 7848  lmbr 7880  lmuni 7902  metelcls 7916  metcnp4 7920  xplm 7925  xpcn 7926  iscms2lem4 7942  bcthlem8 7956  grpidinvlem3 8000  grpideu 8003  grpinveu 8014  sspival 8344  nmounbi 8384  ubthlem3 8475  ubthlem4 8476  ubthlem5 8477  minveclem9 8497  minveclem24 8512  minveclem25 8513  minveclem26 8514  minveclem27 8515  minveclem28 8516  minveclem30 8518  minveclem31 8519  htthlem11 8573  htthlem12 8574  h2hlm 8789  hcau2 8994  ocsh 9095  occllem6 9117  projlem25 9149  projlem26 9150  kbpjt 9819  nlelch 9932  riesz1t 9936  leopmulit 10004  hmopidmch 10017  mdbr2 10161  mdsl0 10174  mdslmd3 10196  csmdsym 10198  atcvatlem 10249  irredlem1 10254  irred 10258  cdj3lem2b 10298
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain