Theorem an1rs 492

Description: Deduction rearranging conjuncts.

Hypothesis

Ref	Expression
an1rs.1	⊢ (((φ ⋀ ψ) ⋀ χ) → θ)

Assertion

Ref	Expression
an1rs	⊢ (((φ ⋀ χ) ⋀ ψ) → θ)

Proof of Theorem an1rs

Step	Hyp	Ref	Expression
1		an23 488	. 2 ⊢ (((φ ⋀ χ) ⋀ ψ) ↔ ((φ ⋀ ψ) ⋀ χ))
2		an1rs.1	. 2 ⊢ (((φ ⋀ ψ) ⋀ χ) → θ)
3	1, 2	sylbi 199	1 ⊢ (((φ ⋀ χ) ⋀ ψ) → θ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  anabsan 507  ordunisssuc 3099  fssres 3659  foco 3698  f1ores 3719  fconstfv 3865  isocnv 3912  f1oiso 3920  oev2 4178  oaordi 4196  oaass 4211  omlimcl 4225  odi 4226  omass 4227  oewordri 4235  oelim2 4238  oaabs 4268  undom 4457  mapenlem1 4509  mapenlem2 4510  mapxpen 4515  mapunen 4522  isfinite2 4564  supmo 4591  unidom 4825  suplem1pr 5181  suplem2pr 5182  recexsrlem 5232  suppsr2 5243  cnegexlem3 5367  axsup 5527  xrlttr 5573  recextlem2 5703  suprleub 6091  dfinfmr 6099  xrsupsslem 6108  xrinfmsslem 6109  supxr2 6114  supxrre 6115  supxrunb1 6121  supxrbnd1 6127  supxrbnd2 6128  supxrleub 6131  uzindOLD 6243  qreccl 6275  iooss1 6340  iooss2 6341  fsequb 6491  recexp 6626  divexp 6630  expmwordi 6637  cau5ii 6949  cvg3i 6955  fsum2mul 7069  fsumcmpndx2 7074  climconsti 7126  2climnni 7134  2climnn0i 7135  climshft2i 7138  iserzshft2i 7139  climrecli 7142  climge0i 7144  climcaui 7188  caucvglem6 7194  cvgcmp3ci 7218  isum1pi 7238  isumreclti 7242  cvgratlem1 7282  cvgratlem2 7283  cvgratlem5 7286  fsum0diaglem2 7289  fsum0diag2 7291  fsum0diag3 7292  fsum0diag4 7293  infxpidmlem10 7594  infdif 7601  tgcl 7654  cldcls 7708  clsval2 7711  0ntr 7728  innei 7762  sncld 7813  bl2in 7869  blin 7878  metcnp 7913  metcn 7915  metcnp3 7922  lmbr 7954  lmuni 7977  metelcls 7991  metcnp4 7996  xplm 8001  xpcn 8002  iscms2lem4 8018  bcthlem8 8032  grpidinvlem3 8076  grpideu 8079  grpinveu 8089  sspival 8422  nmounbi 8464  ubthlem3 8556  ubthlem4 8557  ubthlem5 8558  minveclem9 8578  minveclem24 8593  minveclem25 8594  minveclem26 8595  minveclem27 8596  minveclem28 8597  minveclem30 8599  minveclem31 8600  htthlem11 8655  htthlem12 8656  h2hlm 8874  hcau2 9079  ocsh 9180  occllem6 9202  projlem25 9234  projlem26 9235  kbpj 9904  nlelchi 10018  riesz1 10022  leopmuli 10090  hmopidmchi 10103  mdbr2 10248  mdsl0 10262  mdslmd3i 10284  csmdsymi 10286  atcvatlem 10337  irredlem1 10342  irredi 10346  cdj3lem2b 10389

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