Theorem an1rs 488

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 484	. 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 503  ordunisssuc 3073  fssres 3628  foco 3667  f1ores 3688  fconstfv 3834  isocnv 3881  f1oiso 3889  oev2 4146  oaordi 4164  oaass 4179  omlimcl 4193  odi 4194  omass 4195  oewordri 4203  oelim2 4206  oaabs 4236  undom 4418  mapenlem1 4469  mapenlem2 4470  mapxpen 4475  mapunen 4482  isfinite2 4523  supmo 4550  unidom 4780  suplem1pr 5133  suplem2pr 5134  recexsrlem 5184  suppsr2 5195  cnegextlem3 5319  axsup 5479  xrlttrt 5526  recextlem2 5656  suprleub 6006  dfinfmr 6014  xrsupsslem 6023  xrinfmsslem 6024  supxr2 6029  supxrre 6030  supxrunb1 6036  supxrbnd1 6042  supxrbnd2 6043  supxrleub 6046  uzindOLD 6156  qrecclt 6211  iooss1 6310  iooss2 6311  fsequb 6455  recexpt 6526  divexpt 6530  expmwordit 6537  cau5i 6854  cvg3 6860  fsum2mul 6975  fsumcmpndx2 6980  climconst 7031  2climnn 7039  2climnn0 7040  climshft2 7043  iserzshft2 7044  climrecl 7047  climge0 7049  climcau 7092  caucvglem6 7098  cvgcmp3c 7122  isum1p 7141  isumreclt 7145  cvgratlem1 7185  cvgratlem2 7186  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag3 7195  fsum0diag4 7196  infxpidmlem10 7504  infdif 7511  tgclt 7566  cldcls 7624  clsval2 7627  0ntr 7644  innei 7677  sncld 7726  bl2in 7783  blin 7792  metcnp 7826  metcn 7828  metcnp3 7835  lmbr 7866  lmuni 7886  metelcls 7900  metcnp4 7904  xplm 7909  xpcn 7910  iscms2lem4 7926  bcthlem8 7940  grpidinvlem3 7984  grpideu 7987  grpinveu 7998  sspival 8331  nmounbi 8371  ubthlem3 8462  ubthlem4 8463  ubthlem5 8464  minveclem9 8484  minveclem24 8499  minveclem25 8500  minveclem26 8501  minveclem27 8502  minveclem28 8503  minveclem30 8505  minveclem31 8506  htthlem11 8560  htthlem12 8561  h2hlm 8789  hcau2 8976  ocsh 9072  occllem6 9094  projlem25 9126  projlem26 9127  kbpjt 9796  nlelch 9909  riesz1t 9913  leopmulit 9978  hmopidmch 9990  mdbr2 10133  mdsl0 10145  mdslmd3 10167  csmdsym 10169  atcvatlem 10220  irredlem1 10225  irred 10229  cdj3lem2b 10269

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