Theorem an4s 519

Description: Inference rearranging 4 conjuncts in antecedent.

Hypothesis

Ref	Expression
an4s.1	|- (((ph /\ ps) /\ (ch /\ th)) -> ta)

Assertion

Ref	Expression
an4s	|- (((ph /\ ch) /\ (ps /\ th)) -> ta)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 517	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> ((ph /\ ps) /\ (ch /\ th)))
2		an4s.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
3	1, 2	sylbi 206	1 |- (((ph /\ ch) /\ (ps /\ th)) -> ta)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  anandis 523  anandirs 524  2mo 1490  fnun 3651  f1co 3724  f1oun 3763  f1oco 3764  tfrlem2 3970  tfrlem5 3973  brecop 4367  th3qlem1 4375  oprec 4379  undom 4501  mulclpi 5086  addcmpblnq 5117  mulcmpblnq 5118  mulpipq 5120  ordpipq 5121  mulclpq 5125  mulasspq 5130  distrpqlem 5131  distrpq 5132  ltapq 5141  genpnnp 5173  genpcd 5174  genpnmax 5175  prlem934 5204  addcmpblnr 5246  mulcmpblnr 5248  addsrpr 5249  mulsrpr 5250  ltsrpr 5251  addclsr 5257  mulclsr 5258  addasssr 5262  mulasssr 5264  distrsr 5265  mulgt0sr 5279  addresr 5321  mulresr 5322  axaddopr 5330  axmulopr 5331  axaddass 5342  axmulass 5343  axdistr 5344  add4 5403  2addsub 5454  mul4 5485  muladd 5486  addsub4 5538  sub4 5541  mulsub 5542  muln0 5763  divmuldiv 5838  divdivdiv 5843  recdiv 5848  ltmul12a 5899  lemul12aOLD 5901  ltrec 5944  lerec 5945  lt2msq 5946  le2msq 5963  nnleltp1 6015  rpaddcl 6120  rpmulcl 6121  zaddcl 6247  zmulcl 6262  zltp1le 6263  qaddcl 6321  qmulcl 6323  iooin 6397  ser1add2i 6597  ser1addi 6598  sq11 6718  creur 6832  creui 6833  climge0 7202  climmullem8 7217  iserzgt0 7301  reeff1o 7517  tgcl 7713  innei 7821  islp2 7832  metxp 7919  opnin 7954  iscms2lem3 8076  lmcau 8081  ajmoi 8603  ubthlem12 8624  ubthlem13 8625  spwmo 8740  hvadd4 8988  hvsub4 8989  hlimcauii 9189  pjtheui 9318  shsel3 9362  shscli 9364  shscom 9366  chj4 9541  osumlem2 9662  5oalem3 9684  5oalem5 9686  5oalem6 9687  hoadd4 9793  adjmo 9841  adjsym 9842  cnvadj 9899  bra11 10124  hmopidmchi 10162  mdslmd1lem2 10337  irredlem2 10402  irredi 10405  cdjreui 10443  uninqs 10527  infi1 10532  filintf 10662  fgsb 10663  fgsb2 10668

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 154  df-an 232

Copyright terms: Public domain