Theorem an4s 566

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 564	. 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> ((ph /\ ps) /\ (ch /\ th)))
2		an4s.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
3	1, 2	sylbi 216	1 |- (((ph /\ ch) /\ (ps /\ th)) -> ta)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  anandis 570  anandirs 571  2mo 1851  fnun 4520  f1co 4612  f1oun 4658  f1oco 4661  dfoprab5sf 5058  tfrlem2 5120  tfrlem5 5123  oeoe 5274  brecop 5365  th3qlem1 5373  oprec 5377  undom 5497  mulclpi 6173  addcmpblnq 6204  mulcmpblnq 6205  mulpipq 6207  ordpipq 6208  mulclpq 6212  mulasspq 6217  distrpqlem 6218  distrpq 6219  ltapq 6228  genpnnp 6260  genpcd 6261  genpnmax 6262  prlem934 6291  addcmpblnr 6333  mulcmpblnr 6335  addsrpr 6336  mulsrpr 6337  ltsrpr 6338  addclsr 6344  mulclsr 6345  addasssr 6349  mulasssr 6351  distrsr 6352  mulgt0sr 6366  addresr 6408  mulresr 6409  axaddopr 6417  axmulopr 6418  axaddass 6430  axmulass 6431  axdistr 6432  add4 6491  add4OLD 6492  2addsub 6548  mul4 6581  muladd 6582  muladdOLD 6583  addsub4 6640  sub4 6643  mulsub 6644  mulgt0 6678  mulge0 6868  mulne0 6887  divmuldiv 6956  ltmul12a 7023  lemul12aOLD 7025  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  nnleltp1 7138  rpaddcl 7247  rpmulcl 7248  zaddcl 7374  zmulcl 7389  zltp1le 7390  qaddcl 7449  qmulcl 7451  qreccl 7453  iooin 7539  ser1add2i 7751  ser1addi 7752  sq11 7874  creur 7992  creui 7993  climge0 8372  climmullem8 8387  iserzgt0 8472  tgcl 8894  txuni 8935  innei 9012  islp2 9023  metxp 9111  opnin 9146  iscms2lem3 9269  lmcau 9274  ajmoi 9860  ubthlem12OLD 9884  ubthlem13OLD 9886  spwmo 9999  dif1en 10172  filintf 10274  hvadd4 10537  hvsub4 10538  hlimcauii 10739  pjtheui 10868  shsel3 10912  shscli 10914  shscom 10916  chj4 11091  osumlem2 11214  5oalem3 11236  5oalem5 11238  5oalem6 11239  hoadd4 11347  adjmo 11395  adjsym 11396  cnvadj 11453  bra11 11679  hmopidmchi 11723  mdslmd1lem2 11898  irredlem2 11963  irredi 11966  cdjreui 12004  addltmulALT 12018  dvds2ln 13684  dvdslelem 13692  divalglem6 13701  divalglem8 13703  soxp 13950  poseq 13954  wfr3g 13956  wfrlem11 13967  frr3g 13980  uninqs 14340  infi1 14343  inttr 14384  rzrlzreq 14696  intcont 14914  fgsb 14921  fgsb2 14925  lvsovso 15038  eropreu 15733  frminex 15773  add20 15777  addsubeq4 15778  fzadd2 15791  fzdisj 15793  fzm1 15796  absrdbnd 15799  blhalf 15846  geomcau 15849  iccss2 15856  iimulcl 15874  icoopnst 15876  iocopnst 15877  haustlmu 15906  txsubsp 15912  txmet 15925  sstotbnd 15936  totbndss 15937  bndss 15942  heiborlem32 15986  rrncms 16019  rrntotbnd 16022  phtpyco 16056  phtpcer 16062  pcoloopf 16079  pcohtpy 16083  pi1f 16093  pi1val 16094  isdivrng3 16112  riscer 16142  intidl 16177  smores 16446

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 164  df-an 242

Copyright terms: Public domain