HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem an4s 507
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
StepHypRef Expression
1 an4 505 . 2 |- (((ph /\ ch) /\ (ps /\ th)) <-> ((ph /\ ps) /\ (ch /\ th)))
2 an4s.1 . 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
31, 2sylbi 199 1 |- (((ph /\ ch) /\ (ps /\ th)) -> ta)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  anandis 511  anandirs 512  2mo 1440  fnun 3580  f1co 3652  f1oun 3691  f1oco 3692  tfrlem2 3897  tfrlem5 3900  brecop 4290  th3qlem1 4298  oprec 4302  undom 4418  mulclpi 4993  addcmpblnq 5024  mulcmpblnq 5025  mulpipq 5027  ordpipq 5028  mulclpq 5032  mulasspq 5037  distrpqlem 5038  distrpq 5039  ltapq 5048  genpnnp 5080  genpcd 5081  genpnmax 5082  prlem934 5111  addcmpblnr 5153  mulcmpblnr 5155  addsrpr 5156  mulsrpr 5157  ltsrpr 5158  addclsr 5164  mulclsr 5165  addasssr 5169  mulasssr 5171  distrsr 5172  mulgt0sr 5186  addresr 5228  mulresr 5229  axaddopr 5237  axmulopr 5238  axaddass 5249  axmulass 5250  axdistr 5251  add4t 5310  2addsubt 5361  mul4t 5392  muladdt 5393  addsub4t 5445  sub4t 5448  mulsubt 5449  muln0t 5667  divmuldivt 5736  divdivdivt 5741  recdivt 5746  ltmul12it 5797  lemul12itOLD 5799  ltrect 5832  lerect 5833  lt2msqt 5834  le2msqt 5851  nnleltp1t 5901  zaddclt 6112  zmulclt 6127  zltp1let 6128  qaddclt 6207  qmulclt 6209  rpaddclt 6227  rpmulclt 6228  ser1add2 6275  ser1add 6276  iooint 6309  sq11t 6560  creur 6673  creui 6674  climge0 7049  climmullem8 7063  iserzgt0 7146  reeff1o 7368  tgclt 7566  innei 7677  islp2 7688  metxp 7774  opnin 7809  iscms2lem3 7925  lmcau 7930  ajmoi 8450  ubthlem12 8471  ubthlem13 8472  spwmo 8580  hvadd4t 8826  hvsub4t 8827  hlimcaui 9027  pjtheu 9150  shsel3t 9194  shscl 9196  shscomt 9198  chj4t 9373  osumlem2 9496  5oalem3 9518  5oalem5 9520  5oalem6 9521  hoadd4t 9627  adjmo 9675  adjsymt 9676  cnvadj 9733  bra11 9954  hmopidmch 9990  mdslmd1lem2 10161  irredlem2 10226  irred 10229  cdjreu 10264  uninqs 10342  infi1 10347  filintf 10443  fgsb 10444  fgsb2 10449
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