Theorem com24 37

Description: Commutation of antecedents. Swap 2nd and 4th.

Hypothesis

Ref	Expression
com4.1	|- (ph -> (ps -> (ch -> (th -> ta))))

Assertion

Ref	Expression
com24	|- (ph -> (th -> (ch -> (ps -> ta))))

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . . 4 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	com34 36	. . 3 |- (ph -> (ps -> (th -> (ch -> ta))))
3	2	com23 32	. 2 |- (ph -> (th -> (ps -> (ch -> ta))))
4	3	com34 36	1 |- (ph -> (th -> (ch -> (ps -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  tfrlem5 3915  tfrlem9 3919  omcl 4171  oecl 4172  omordi 4197  oeordi 4214  nnmcl 4230  nnecl 4231  nnaordex 4249  nnawordex 4250  fundmen 4428  pssnn 4534  fiint 4559  fiintOLD 4560  r1ord 4655  zorn2lem7 4794  unxpdomlem 4843  genpnnp 5108  prlem934 5139  ltexprlem7 5148  prlem936b 5154  suplem1pr 5161  suppsr2 5223  divne0t 5729  climsqueeze 7140  climsqueeze2 7141  caucvg 7163  reccnv 7218  expcnvlem6 7232  fsum0diag2 7259  fsum0diag4 7261  infpnlem1 7506  infxpidmlem12 7563  subtop 7646  cnsscnp 7772  lmuni 7951  cmsss 7997  bcthlem20 8018  grpinveu 8064  blocnilem 8464  elspansn4t 9496  osumlem4 9581  atoml 10309  mdsymlem3 10332  mdsymlem5 10334  uninqs 10441  fiiu 10453  fiiuOLD 10454  fiiu2 10488  fiiu2OLD 10489  cnrsfin 10509  cnrscoa 10510  homcard 10539  set2elt 10545  top2ind 10548  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  cmpmon 10743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain