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

Step	Hyp	Ref	Expression
1		an23 485	. 2 |- (((ph /\ ch) /\ ps) <-> ((ph /\ ps) /\ ch))
2		an1rs.1	. 2 |- (((ph /\ ps) /\ ch) -> th)
3	1, 2	sylbi 199	1 |- (((ph /\ ch) /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anabsan 504  ordunisssuc 3080  fssres 3640  foco 3679  f1ores 3700  fconstfv 3846  isocnv 3893  f1oiso 3901  oev2 4159  oaordi 4177  oaass 4192  omlimcl 4206  odi 4207  omass 4208  oewordri 4216  oelim2 4219  oaabs 4249  undom 4431  mapenlem1 4482  mapenlem2 4483  mapxpen 4488  mapunen 4495  isfinite2 4536  supmo 4563  unidom 4795  suplem1pr 5148  suplem2pr 5149  recexsrlem 5199  suppsr2 5210  cnegextlem3 5334  axsup 5494  xrlttrt 5540  recextlem2 5670  suprleub 6020  dfinfmr 6028  xrsupsslem 6037  xrinfmsslem 6038  supxr2 6043  supxrre 6044  supxrunb1 6050  supxrbnd1 6056  supxrbnd2 6057  supxrleub 6060  uzindOLD 6170  qrecclt 6228  iooss1 6328  iooss2 6329  fsequb 6473  recexpt 6545  divexpt 6549  expmwordit 6556  cau5i 6883  cvg3 6889  fsum2mul 7005  fsumcmpndx2 7010  climconst 7062  2climnn 7070  2climnn0 7071  climshft2 7074  iserzshft2 7075  climrecl 7078  climge0 7080  climcau 7125  caucvglem6 7131  cvgcmp3c 7157  isum1p 7177  isumreclt 7181  cvgratlem1 7221  cvgratlem2 7222  cvgratlem5 7225  fsum0diaglem2 7228  fsum0diag2 7230  fsum0diag3 7231  fsum0diag4 7232  infxpidmlem10 7540  infdif 7547  tgclt 7603  cldcls 7661  clsval2 7664  0ntr 7681  innei 7715  sncld 7766  bl2in 7825  blin 7834  metcnp 7870  metcn 7872  metcnp3 7879  lmbr 7911  lmuni 7934  metelcls 7948  metcnp4 7953  xplm 7958  xpcn 7959  iscms2lem4 7975  bcthlem8 7989  grpidinvlem3 8033  grpideu 8036  grpinveu 8047  sspival 8383  nmounbi 8424  ubthlem3 8515  ubthlem4 8516  ubthlem5 8517  minveclem9 8537  minveclem24 8552  minveclem25 8553  minveclem26 8554  minveclem27 8555  minveclem28 8556  minveclem30 8558  minveclem31 8559  htthlem11 8613  htthlem12 8614  h2hlm 8834  hcau2 9043  ocsh 9144  occllem6 9166  projlem25 9198  projlem26 9199  kbpjt 9871  nlelch 9985  riesz1t 9989  leopmulit 10057  hmopidmch 10070  mdbr2 10214  mdsl0 10228  mdslmd3 10250  csmdsym 10252  atcvatlem 10303  irredlem1 10308  irred 10312  cdj3lem2b 10355

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