Theorem an1rs 491

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 487	. 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 506  ordunisssuc 3090  fssres 3650  foco 3689  f1ores 3710  fconstfv 3856  isocnv 3903  f1oiso 3911  oev2 4169  oaordi 4187  oaass 4202  omlimcl 4216  odi 4217  omass 4218  oewordri 4226  oelim2 4229  oaabs 4259  undom 4445  mapenlem1 4496  mapenlem2 4497  mapxpen 4502  mapunen 4509  isfinite2 4559  isfinite2OLD 4560  supmo 4592  unidom 4825  suplem1pr 5180  suplem2pr 5181  recexsrlem 5231  suppsr2 5242  cnegextlem3 5366  axsup 5526  xrlttrt 5572  recextlem2 5702  suprleub 6068  dfinfmr 6076  xrsupsslem 6085  xrinfmsslem 6086  supxr2 6091  supxrre 6092  supxrunb1 6098  supxrbnd1 6104  supxrbnd2 6105  supxrleub 6108  uzindOLD 6217  qrecclt 6281  iooss1 6381  iooss2 6382  fsequb 6531  recexpt 6603  divexpt 6607  expmwordit 6614  cau5i 6924  cvg3 6930  fsum2mul 7044  fsumcmpndx2 7049  climconst 7101  2climnn 7109  2climnn0 7110  climshft2 7113  iserzshft2 7114  climrecl 7117  climge0 7119  climcau 7163  caucvglem6 7169  cvgcmp3c 7193  isum1p 7213  isumreclt 7217  cvgratlem1 7257  cvgratlem2 7258  cvgratlem5 7261  fsum0diaglem2 7264  fsum0diag2 7266  fsum0diag3 7267  fsum0diag4 7268  infxpidmlem10 7569  infdif 7576  tgclt 7630  cldcls 7686  clsval2 7689  0ntr 7706  innei 7740  sncld 7791  bl2in 7847  blin 7856  metcnp 7891  metcn 7893  metcnp3 7900  lmbr 7932  lmuni 7955  metelcls 7969  metcnp4 7974  xplm 7979  xpcn 7980  iscms2lem4 7996  bcthlem8 8010  grpidinvlem3 8054  grpideu 8057  grpinveu 8067  sspival 8400  nmounbi 8442  ubthlem3 8534  ubthlem4 8535  ubthlem5 8536  minveclem9 8556  minveclem24 8571  minveclem25 8572  minveclem26 8573  minveclem27 8574  minveclem28 8575  minveclem30 8577  minveclem31 8578  htthlem11 8633  htthlem12 8634  h2hlm 8852  hcau2 9057  ocsh 9158  occllem6 9180  projlem25 9212  projlem26 9213  kbpjt 9882  nlelch 9996  riesz1t 10000  leopmulit 10068  hmopidmch 10081  mdbr2 10226  mdsl0 10240  mdslmd3 10262  csmdsym 10264  atcvatlem 10315  irredlem1 10320  irred 10324  cdj3lem2b 10367

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