Theorem com24 37

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

Hypothesis

Ref	Expression
com4.1	⊢ (φ → (ψ → (χ → (θ → τ))))

Assertion

Ref	Expression
com24	⊢ (φ → (θ → (χ → (ψ → τ))))

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . . 4 ⊢ (φ → (ψ → (χ → (θ → τ))))
2	1	com34 36	. . 3 ⊢ (φ → (ψ → (θ → (χ → τ))))
3	2	com23 32	. 2 ⊢ (φ → (θ → (ψ → (χ → τ))))
4	3	com34 36	1 ⊢ (φ → (θ → (χ → (ψ → τ))))

Syntax hints:   → wi 3

This theorem is referenced by:  tfrlem5 4216  tfrlem9 4220  omcl 4307  oecl 4308  omordi 4333  oeordi 4350  nnmcl 4370  nnecl 4371  nnaordex 4389  nnawordex 4390  fundmen 4569  ac6sfilem3 4590  pssnn 4681  fiint 4703  r1ord 4801  zorn2lem7 4940  unxpdomlem 4993  genpnnp 5262  prlem934 5293  ltexprlem7 5302  prlem936b 5308  suplem1pr 5315  suppsr2 5377  divne0 5875  climsqueeze 7343  climsqueeze2 7344  caucvgi 7366  reccnv 7422  expcnvlem6 7436  fsum0diag2 7464  fsum0diag4 7466  infpnlem1 7718  infxpidmlem12 7775  subtop 7858  cnsscnp 7982  metequiv 8091  lmuni 8162  cmsss 8208  bcthlem20 8229  grpinveu 8281  vacnlem3 8584  blocnilem 8719  elspansn4 9772  osumlem4 9859  atomli 10591  mdsymlem3 10614  mdsymlem5 10616  uninqs 10730  fiiu 10738  imgfldref2 10768  isunscov 10796  prj1 10809  set2elt 10827  fiiu2 10852  ununr 10955  uznzr 10967  cnrsfin 11012  cnrscoa 11013  homcard 11045  top2ind 11050  efilcp2 11087  cnfilca 11088  bwt2 11123  usinuniop 11128  altretop 11144  cmpmon 11270  com25 11327  ordiso 11426  hausnei2 11471  cnpnei 11472  compsublem 11487  cncomp 11494  alexsublem3 11498  reconnlem1 11507  comppfsc 11578  neibastop1 11579  neibastop2lem2 11581  neibastop2lem4 11583  topmtcl 11586  fnejoin2 11592  isufil2 11650  filssufillem 11655  filufint 11659  flimopn 11679  limfilcf 11683  hausfillim 11685  cnpfillim 11686  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomp 11733  ufcomp 11734  inficl 11849  sdclem2 11876  sdc 11877  blhalf 11911  txbas 11973  txcn 11979  heiborlem23 12033

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

Copyright terms: Public domain